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

We present a formal verification of Wolstenholme’s theorem – $\left(\genfrac{}{}{0px}{}{2p}{p}\right)\equiv 2(\mathrm{m}\mathrm{o}\mathrm{d}{p}^3)$ for prime $p\ge 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}\mathrm{/}p\mathbb{Z}$. The formalization comprises nine lemmas across approximately 800 lines of Lean, with zero $\mathtt{\text{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.