WieferichMirimanoffPrime.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 2 contain sorry, 0 declared as axioms

Can a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{p^2}$?

A prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$ is a Wieferich prime (the only known examples are $1093$ and $3511$). A prime $p$ with $3^{p-1} \equiv 1 \pmod{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.

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)

Imports (1)

FormalConjecturesUtil

theorem WieferichMirimanoffPrime.exists_isWieferichPrime_and_isMirimanoffPrime Can a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{p^2}$ simultaneously? sorry line 50 source
Source documentation
Can a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{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).

L4DEL explanation
Can a prime $p$ satisfy $2^{p-1} \equiv 1 \pmod{p^2}$ and $3^{p-1} \equiv 1 \pmod{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).
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, IsWieferichPrime, IsMirimanoffPrime
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem exists_isWieferichPrime_and_isMirimanoffPrime :
    answer(sorry) ↔ ∃ p : ℕ, IsWieferichPrime p ∧ IsMirimanoffPrime p := by
…
```
Mentions: IsWieferichPrime, IsMirimanoffPrime
theorem WieferichMirimanoffPrime.isMirimanoffPrime_iff Are $11$ and $1006003$ the only Mirimanoff primes? sorry line 59 source
Source documentation
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}$.

depends on sorry what this means
Statement uses: Iff, True, Nat, IsMirimanoffPrime, Or, Eq, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isMirimanoffPrime_iff :
    answer(sorry) ↔ ∀ p, IsMirimanoffPrime p ↔ p = 11 ∨ p = 1006003 := by
…
```
Mentions: IsMirimanoffPrime
theorem WieferichMirimanoffPrime.isMirimanoffPrime_and_not_isWieferichPrime_11 The prime $11$ is a Mirimanoff prime but not a Wieferich prime line 65 source
Source documentation
The prime $11$ is a Mirimanoff prime but not a Wieferich prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, IsMirimanoffPrime, OfNat.ofNat, Nat, Not, IsWieferichPrime
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isMirimanoffPrime_and_not_isWieferichPrime_11 :
    IsMirimanoffPrime 11 ∧ ¬ IsWieferichPrime 11 := by
…
```
Mentions: IsMirimanoffPrime, IsWieferichPrime
theorem WieferichMirimanoffPrime.isMirimanoffPrime_and_not_isWieferichPrime_1006003 The prime $1006003$ is a Mirimanoff prime but not a Wieferich prime line 71 source
Source documentation
The prime $1006003$ is a Mirimanoff prime but not a Wieferich prime.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: And, IsMirimanoffPrime, OfNat.ofNat, Nat, Not, IsWieferichPrime
Proof uses: And.intro, IsWieferichPrimeBase.mk, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_2, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Bool.false, Mathlib.Meta.NormNum.minFacHelper_3, Mathlib.Meta.NormNum.minFacHelper_0, absurd, Dvd.dvd, HPow.hPow, HSub.hSub, False, IsWieferichPrimeBase.sq_dvd_pow_sub_one
12 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem isMirimanoffPrime_and_not_isWieferichPrime_1006003 :
    IsMirimanoffPrime 1006003 ∧ ¬ IsWieferichPrime 1006003 :=
…
```
Mentions: IsMirimanoffPrime, IsWieferichPrime
theorem WieferichMirimanoffPrime.not_isMirimanoffPrime_two Neither $2$ nor $3$ is a Mirimanoff prime, so no hypothesis excluding them is needed in the statement of the problem line 78 source
Source documentation
Neither $2$ nor $3$ is a Mirimanoff prime, so no hypothesis excluding them is needed in the statement of the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, IsMirimanoffPrime, OfNat.ofNat, Nat
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem not_isMirimanoffPrime_two : ¬ IsMirimanoffPrime 2 := by
…
```
Mentions: IsMirimanoffPrime
theorem WieferichMirimanoffPrime.not_isWieferichPrime_three The prime $3$ is not a Wieferich prime line 83 source
Source documentation
The prime $3$ is not a Wieferich prime. For $2$, see WieferichPrime.not_isWieferichPrime_two.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, IsWieferichPrime, OfNat.ofNat, Nat
Proof uses: of_decide_eq_true, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem not_isWieferichPrime_three : ¬ IsWieferichPrime 3 := by
…
```
Mentions: IsWieferichPrime