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

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.