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

arXiv: https://arxiv.org/abs/2604.16507 · HTML: https://mlsanity.com/paper/2604.16507/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 Apr 2026.

## Built on by (most cited first, 1 of 1)

- [Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1](https://mlsanity.com/paper/2604.17229/) (2026)

## Abstract (arXiv)

We present a formal verification of Wolstenholme's theorem -- binom2pp equiv 2 pmodp3 for prime p ≥ 5 -- in Lean~4 with Mathlib. The proof proceeds by expanding the shifted factorial product prodk=1p-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 mathbbZ/pmathbbZ. The formalization comprises nine lemmas across approximately 800 lines of Lean, with zero textttsorry 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.