Can a prime p satisfy 2^p-1 ≡ 1 pmodp^2 and 3^p-1 ≡ 1 pmodp^2?

The question

exists_isWieferichPrime_and_isMirimanoffPrime. Can a prime $p$ satisfy $2^{p-1}\equiv 1(\mathrm{mod}{p}^2)$ and $3^{p-1}\equiv 1(\mathrm{mod}{p}^2)$ simultaneously? That is, does there exist a prime $p$ that is both a Wieferich prime and a Mirimanoff prime? Wikipedia's list of unsolved problems poses this question, citing J. B. Dobson, On Lerch's formula for the Fermat quotient. Lenstra gave a heuristic argument against the existence of such a prime (see Dobson, Section 9).

isMirimanoffPrime_iff. Are $11$ and $1006003$ the only Mirimanoff primes? They are the only known ones: Dorais and Klyve found no other below $9.7\times 10^{14}$.

A prime $p$ with $2^{p-1}\equiv 1(\mathrm{mod}{p}^2)$ is a Wieferich prime (the only known examples are $1093$ and $3511$). A prime $p$ with $3^{p-1}\equiv 1(\mathrm{mod}{p}^2)$ is a Mirimanoff prime (the only known examples are $11$ and $1006003$). It is an open question whether a prime can satisfy both congruences simultaneously. Lenstra gave a heuristic argument against this.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Wikipedia.WieferichMirimanoffPrime (2 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem exists_isWieferichPrime_and_isMirimanoffPrime :
    answer(sorry) ↔ ∃ p : ℕ, IsWieferichPrime p ∧ IsMirimanoffPrime p

theorem isMirimanoffPrime_iff :
    answer(sorry) ↔ ∀ p, IsMirimanoffPrime p ↔ p = 11 ∨ p = 1006003

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Wikipedia, List of unsolved problems in mathematics
• Wikipedia, Wieferich prime
• J. B. Dobson, On Lerch's formula for the Fermat quotient
• F. G. Dorais and D. Klyve, A Wieferich prime search up to $6.7\times 10^{15}$, J. Integer Seq. 14 (2011), Article 11.9.2.
• OEIS A001220 (Wieferich primes)
• OEIS A014127 (Mirimanoff primes)

Source and licence

Imported from Formal Conjectures (Wikipedia), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.