Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
This work provides a formal proof of a classical number theory result for the Lean 4 community, but the theorem itself is well-known and the proof is incremental.
The authors present the first formal verification of Wolstenholme's theorem in Lean 4, comprising approximately 800 lines of code with zero sorry declarations.
We present a formal verification of Wolstenholme's theorem -- $\binom{2p}{p} \equiv 2 \pmod{p^3}$ for prime $p \geq 5$ -- in Lean~4 with Mathlib. The proof proceeds by expanding the shifted factorial product $\prod_{k=1}^{p-1}(p+k)$ to second order in $p$, identifying the quadratic coefficient as the second elementary symmetric product, and showing its divisibility by $p$ via power sum vanishing in $\mathbb{Z}/p\mathbb{Z}$. The formalization comprises nine lemmas across approximately 800 lines of Lean, with zero \texttt{sorry} declarations. To our knowledge, this is the first formal verification of Wolstenholme's theorem in Lean~4. The proof was discovered through a collaboration between a relational analogy engine for theorem proving and human-directed formalization.