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².
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.
The 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.
Proof architecture
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 source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.
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_zerowolstenholmeTheoremExact 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 : WolstenholmeTheoremStatementResult 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.
Continue the mathematics
The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.
Independent publication review
Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.
Independent 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.
Independent 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.