Number theory · formal theorem
For every prime p > 3, the sum 1 + 1/2 + ⋯ + 1/(p − 1), with reciprocals interpreted modulo p², is 0 modulo p².
Scope: Wolstenholme's theorem in modular reciprocal-sum form: for every prime p > 3, the finite reciprocal harmonic sum through p − 1 is zero in ZMod (p²).
Exact formal proposition
This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.
def WolstenholmeTheoremStatement : Prop :=
∀ p : ℕ, p.Prime → 3 < p → harmonicReciprocalSumMod p = 0harmonicReciprocalSumMod noncomputable def harmonicReciprocalSumMod (p : ℕ) : ZMod (p ^ 2) :=
∑ k ∈ Finset.Icc 1 (p - 1), ((k : ZMod (p ^ 2))⁻¹)The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.
theorem wolstenholmeTheorem : WolstenholmeTheoremStatementProof route
The proof pairs complementary residues, reduces the paired sum modulo p, uses symmetry and a finite-field power sum, then lifts the resulting zero back to modulo p squared.
These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.
2H = pS in ZMod (p²)
Pairing k with p − k rewrites the two reciprocal terms over a shared denominator and exposes a common factor p. Summing the exact pair identity gives 2H = pS in ZMod (p²); the paired terms do not individually cancel to zero.
reciprocal_pair_sum_eqtwo_mul_harmonicReciprocalSumMod_eq_p_mul_sum
cast(S) = -∑ k ∈ Icc 1 (p - 1), k⁻² in ZMod p
Reducing S from ZMod (p²) to ZMod p turns each paired denominator contribution into a negative inverse square. Thus S reduces to the negative sum of k⁻² over the nonzero residues.
castHom_inv_of_isUnitcastHom_pair_denominator_invcastHom_pair_sum_eq_zero
∑ u ∈ (ZMod p)ˣ, u² = 0
The nonzero residues are exactly the units of ZMod p, and inversion permutes that finite set. Reindexing therefore converts the inverse-square sum into the square power sum, which vanishes for p > 3 by the finite-field power-sum identity.
sum_Icc_inv_sq_eq_sum_units_inv_sqsum_units_inv_sq_eq_sum_units_sqzmod_prime_units_sum_sq_eq_zeroFiniteField.sum_pow_units
cast(S) = 0 ⇒ pS = 0; 2H = pS ⇒ H = 0 in ZMod (p²)
Because S reduces to zero modulo p, multiplying it by p gives zero in ZMod (p²). Combining pS = 0 with 2H = pS gives 2H = 0, and the unit 2 can be cancelled because p > 3, leaving H = 0.
p_mul_eq_zero_of_castHom_eq_zerop_mul_pair_sum_eq_zerotwo_isUnit_zmod_prime_sqharmonicReciprocalSumMod_eq_zero_of_p_mul_pair_sum_eq_zerowolstenholmeTheoremThe theorem at a glance
Accessible transcript
For prime p > 3: ∑ k = 1 to p - 1 of k⁻¹ = 0 in ZMod(p²)
For every prime p > 3, the sum of the modular inverses of k from 1 through p − 1 is zero in ZMod(p²); every inverse is taken modulo p², so the complete harmonic row vanishes modulo p², not merely modulo p. For p = 5 in modulus 25, the inverses 1, 13, 17, and 19 sum to 50, hence zero modulo 25. The proof pairs k with p − k to obtain 2H = pS, reduces S modulo p to a negative inverse-square sum, uses inversion as a permutation of the nonzero units and the finite-field square power sum, then lifts S = 0 modulo p and cancels the invertible factor 2. The formal theorem proves this modular reciprocal-sum form, not the binomial-coefficient congruence modulo p³, an equivalence between those formulations, or vanishing of the ordinary real harmonic sum.
CLASSICAL NUMBER THEORY · MODULAR ARITHMETIC
WOLSTENHOLME’S THEOREM
THE EXTRA POWER
p → p²
The complete harmonic row vanishes modulo p²—not merely modulo p.
FOR EVERY PRIME p > 3
∑ₖ₌₁ᵖ⁻¹ k⁻¹ = 0 in ZMod(p²)
Every inverse is taken modulo p².
TRY p = 5 · MODULUS 25
1⁻¹, 2⁻¹, 3⁻¹, 4⁻¹ ≡ 1, 13, 17, 19
1 + 13 + 17 + 19 = 50 ≡ 0 (mod 25)
HOW THE PROOF MOVES
1 · PAIR COMPLEMENTS
k ↔ p − k · expose one factor p · 2H = pS
2 · REDUCE MODULO p
S becomes a negative inverse-square sum.
3 · SUM OVER ALL NONZERO UNITS
Inversion permutes the units · ∑u² = 0
4 · LIFT AND CANCEL
S = 0 modulo p ⇒ pS = 0 modulo p² · 2H = pS ⇒ H = 0
EXACT SCOPE
The modular reciprocal-sum form. Not the binomial-coefficient congruence modulo p³. Not an equivalence proof. Not a statement that the ordinary real harmonic sum is zero.
Mathematical illustration
For prime p > 3: 1 + 1/2 + ⋯ + 1/(p - 1) = 0 in ZMod (p²)
For a prime p > 3, every k from 1 through p − 1 is a unit modulo p². The sum of all their inverses is zero in ZMod(p²); individual inverse terms need not vanish, and the statement concerns modular arithmetic rather than an ordinary real harmonic sum.
Result boundary
Wolstenholme's theorem in modular reciprocal-sum form: for every prime p > 3, the finite reciprocal harmonic sum through p − 1 is zero in ZMod (p²).
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
Continue the mathematics
The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.
Review record
Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.
The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
The formal declaration was accepted against the named theorem and its exact variant.
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
The first-party source link is pinned to the checked package commit and exact Lean file.
A validated accepted-result record binds the four reviews to the checked formalization.