Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
Alexandre Linhares
cs.LO
Apr 14, 2026 · v2
TL;DR
Formalizes Wolstenholme's theorem in Lean 4 with Mathlib, using an analogy-based engine over Mathlib proof states to discover tactics.
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 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.
Problem
Wolstenholme's theorem, that binom(2p,p) ≡ 2 mod p^3 for primes p ≥ 5, had not been formalized in major libraries such as Mathlib.
Approach
The proof reduces the congruence to a statement about the shifted product ∏(p+k). It expands this product to second order in p, identifies the quadratic coefficient as the second elementary symmetric product e2, and proves p divides e2 via power-sum vanishing in Z/pZ. Deep Vision, a relational analogy engine, matched proof states against 217,133 states extracted from Mathlib and transferred tactics. It worked alongside Claude Code and human-directed formalization.
Results
The result is a self-contained Lean 4 file of roughly 660–800 lines with no sorry or axiom declarations. Deep Vision autonomously found a 7-step simp/ring_nf tactic chain for the e2 recurrence lemma.
