WieferichPrime.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

10 declarations, 0 contain sorry, 0 declared as axioms

Wieferich primes

A prime $p$ is a Wieferich prime to base $a$ if $p^2$ divides $a^{p-1} - 1$, i.e. if the congruence $a^{p-1} \equiv 1 \pmod{p}$ of Fermat's little theorem holds modulo $p^2$. A Wieferich prime is a Wieferich prime to base $2$. The only known Wieferich primes are $1093$ and $3511$. A Mirimanoff prime is a Wieferich prime to base $3$. The only known Mirimanoff primes are $11$ and $1006003$.

References:

Wikipedia, Wieferich prime
OEIS A001220 (Wieferich primes)
OEIS A014127 (Mirimanoff primes)
D. Mirimanoff, Sur le dernier théorème de Fermat, C. R. Acad. Sci. Paris 150 (1910), 204–206.

Imports (2)

Imported by 1 file

FormalConjecturesForMathlib.lean

structure IsWieferichPrimeBase Wieferich prime to base a A prime $p$ is a Wieferich prime to base $a$ if $p^2 \mid a^{p-1} - 1$, i.e. if $a^{p-1} \equiv 1 \pmod{p^2}$ line 49 source
Source documentation
Wieferich prime to base a A prime $p$ is a Wieferich prime to base $a$ if $p^2 \mid a^{p-1} - 1$, i.e. if $a^{p-1} \equiv 1 \pmod{p^2}$.
The subtraction is truncated, so, as with Nat.ProbablePrime, every prime is a Wieferich prime to base $0$. For a ≠ 0 the definition agrees with the congruence, see isWieferichPrimeBase_iff_pow_modEq.

standard axioms: propext what this means
Statement uses: Nat
```
structure IsWieferichPrimeBase (a p : ℕ) : Prop where
…
```
instance (instance at line 53) line 53 source
theorem IsWieferichPrimeBase.of_pow_modEq line 60 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Nat.ModEq, HPow.hPow, OfNat.ofNat, HSub.hSub, IsWieferichPrimeBase
Proof uses: IsWieferichPrimeBase.mk, Nat.ModEq.dvd', Nat.ModEq.symm
14 instances, coercions and auxiliary constants left out.
theorem IsWieferichPrimeBase.pow_modEq line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, IsWieferichPrimeBase, Ne, OfNat.ofNat, Nat.ModEq, HPow.hPow, HSub.hSub
Proof uses: Nat.ModEq.symm, Iff.mpr, Dvd.dvd, Nat.modEq_iff_dvd', Nat.one_le_pow, Nat.pos_of_ne_zero, IsWieferichPrimeBase.sq_dvd_pow_sub_one
17 instances, coercions and auxiliary constants left out.
theorem IsWieferichPrimeBase.of_modEq_one Every prime p is a Wieferich prime to any base a ≡ 1 [MOD p ^ 2] line 68 source
Source documentation
Every prime p is a Wieferich prime to any base a ≡ 1 [MOD p ^ 2].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, Nat.ModEq, HPow.hPow, OfNat.ofNat, IsWieferichPrimeBase
Proof uses: IsWieferichPrimeBase.of_pow_modEq, Eq.mp, HSub.hSub, congrArg, one_pow, Nat.ModEq.pow
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem of_modEq_one (hp : p.Prime) (h : a ≡ 1 [MOD p ^ 2]) : IsWieferichPrimeBase a p :=
…
```
Mentions: IsWieferichPrimeBase
theorem isWieferichPrimeBase_iff_pow_modEq For a nonzero base a, being a Wieferich prime to base a is the congruence a ^ (p - 1) ≡ 1 [MOD p ^ 2] line 75 source
Source documentation
For a nonzero base a, being a Wieferich prime to base a is the congruence a ^ (p - 1) ≡ 1 [MOD p ^ 2]. This fails for a = 0: see isWieferichPrimeBase_zero_iff.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Ne, OfNat.ofNat, Iff, IsWieferichPrimeBase, And, Nat.Prime, Nat.ModEq, HPow.hPow, HSub.hSub
Proof uses: Iff.intro, And.intro, IsWieferichPrimeBase.prime, IsWieferichPrimeBase.pow_modEq, IsWieferichPrimeBase.of_pow_modEq, And.left, And.right
14 instances, coercions and auxiliary constants left out.
```
theorem isWieferichPrimeBase_iff_pow_modEq {a p : ℕ} (ha : a ≠ 0) :
    IsWieferichPrimeBase a p ↔ p.Prime ∧ a ^ (p - 1) ≡ 1 [MOD p ^ 2] :=
…
```
Mentions: IsWieferichPrimeBase
theorem isWieferichPrimeBase_zero_iff Every prime is a Wieferich prime to base 0, because 0 ^ (p - 1) - 1 = 0 in ℕ line 81 source
Source documentation
Every prime is a Wieferich prime to base 0, because 0 ^ (p - 1) - 1 = 0 in ℕ.

standard axioms: propext what this means
Statement uses: Nat, Iff, IsWieferichPrimeBase, OfNat.ofNat, Nat.Prime
Proof uses: Iff.intro, IsWieferichPrimeBase.prime, IsWieferichPrimeBase.mk, of_eq_true, Dvd.dvd, HPow.hPow, HSub.hSub, Eq.trans, True, congrArg, congrFun', MonoidWithZero, zero_pow, Nat.sub_ne_zero_of_lt, Nat.Prime.one_lt, Nat.sub_eq_zero_of_le, LE.le
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isWieferichPrimeBase_zero_iff {p : ℕ} : IsWieferichPrimeBase 0 p ↔ p.Prime :=
…
```
Mentions: IsWieferichPrimeBase
theorem isWieferichPrimeBase_one_iff Every prime is a Wieferich prime to base 1 line 86 source
Source documentation
Every prime is a Wieferich prime to base 1.

standard axioms: propext what this means
Statement uses: Nat, Iff, IsWieferichPrimeBase, OfNat.ofNat, Nat.Prime
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, And, Dvd.dvd, HPow.hPow, HSub.hSub, one_pow, Nat.sub_self, and_true, iff_self
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isWieferichPrimeBase_one_iff {p : ℕ} : IsWieferichPrimeBase 1 p ↔ p.Prime := by
…
```
Mentions: IsWieferichPrimeBase
abbrev IsWieferichPrime Wieferich prime A Wieferich prime is a prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $2$ line 94 source
Source documentation
Wieferich prime A Wieferich prime is a prime $p$ with $2^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $2$.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: IsWieferichPrimeBase, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev IsWieferichPrime (p : ℕ) : Prop := IsWieferichPrimeBase 2 p
```
Mentions: IsWieferichPrimeBase
abbrev IsMirimanoffPrime Mirimanoff prime A Mirimanoff prime is a prime $p$ with $3^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $3$ line 102 source
Source documentation
Mirimanoff prime A Mirimanoff prime is a prime $p$ with $3^{p-1} \equiv 1 \pmod{p^2}$, i.e. a Wieferich prime to base $3$. The name comes from Mirimanoff's 1910 result that a failure of the first case of Fermat's Last Theorem for the exponent $p$ forces this congruence.

standard axioms: propext what this means
Statement uses: Nat
Proof uses: IsWieferichPrimeBase, OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
```
abbrev IsMirimanoffPrime (p : ℕ) : Prop := IsWieferichPrimeBase 3 p
```
Mentions: IsWieferichPrimeBase