Papers With

← All papers
First page of Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4

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

Alexandre Linhares

cs.LO Apr 14, 2026 · v1
formalization number-theory
Read PDF arXiv abstract Code
TL;DR
First Lean 4 + Mathlib formal proof of Wolstenholme's theorem (~800 lines, zero sorry).
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.
Problem

Wolstenholme's theorem (that the binomial coefficient C(2p,p) is congruent to 2 mod p^3 for primes p >= 5) is a classical result in number theory, but it has not been formally verified in Lean 4 or any major formal mathematics library.

Approach

The proof proceeds by expanding the shifted factorial product 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 Z/pZ. The formalization in Lean 4 with Mathlib comprises nine lemmas across approximately 800 lines with zero sorry declarations. The proof was discovered through collaboration between a relational analogy engine for theorem proving and human-directed formalization.

Results

This is the first formal verification of Wolstenholme's theorem in Lean 4. The formalization is approximately 800 lines of Lean code with zero sorry declarations, contained in a single self-contained file.