Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4

TL;DR

This paper provides the first formal proof of Wolstenholme's theorem in Lean 4, verifying a key number theory result through detailed formalization without any gaps.

Contribution

It introduces a complete formal verification of Wolstenholme's theorem in Lean 4, demonstrating the theorem's proof structure and implementation in proof assistant.

Findings

Formal proof comprises nine lemmas and about 800 lines of Lean code.

The proof confirms the divisibility of the quadratic coefficient by p.

No gaps or 'sorry' declarations remain in the formalization.

Abstract

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.