Lean evidence record
Wolstenholme’s Theorem: Lean evidence
This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.
Exact formal proposition
Hypotheses and conclusion
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 = 0Definitions used in this proposition
harmonicReciprocalSumMod
noncomputable def harmonicReciprocalSumMod (p : ℕ) : ZMod (p ^ 2) :=
∑ k ∈ Finset.Icc 1 (p - 1), ((k : ZMod (p ^ 2))⁻¹)Lean wrapper declaration
The checked endpoint names the expanded proposition above. Both come from the same commit-pinned source.
theorem wolstenholmeTheorem : WolstenholmeTheoremStatementLine 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.
Technical evidence record
Source identity, checker results, and assumptions
- Main Lean declaration
wolstenholmeTheorem- Source commit
ee454aff99d3
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.known-wolstenholme-theorem.endpoint.v002- Accepted-result title
- Accepted Result: Wolstenholme's Theorem
- Accepted-result status
- Accepted formalization of a known theorem
- Accepted-result boundary
- This target records 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^2). Non-claim: This is not the binomial coefficient formulation or an equivalence proof. Non-claim: This accepted-result record does not establish novelty and does not by itself authorize public export or deployment.
- Declarations covered by recorded evidence
AtlasKnownTheorems.WolstenholmeTheorem.wolstenholmeTheoremAtlasKnownTheorems.WolstenholmeTheorem.WolstenholmeTheoremStatement- Lean build
- passed
- Recorded build time
- 2.3 s one machine-dependent evidence run, not a benchmark
- Evidence collected
- · clean-source provenance recorded
- Unfinished proof check
- passed
- Lean toolchain
leanprover/lean4:v4.29.1- Recorded source commit
ee454aff99d3a2495e3a0073d434aab73e39c15c- Source SHA-256
sha256:1cc9bc40ddbed932b39affd6e9bd498e72e06e8f0b5e25fc8d995b05f1277a53- Statement alignment
- accepted
Lean foundations
Standard foundations used by the proof
Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.
Classical.choiceQuot.soundpropext
Files and machine-readable evidence
Reproduce or inspect the recorded check
Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.
Review results
Publication reviews accepted
All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.
Read the publication-review details