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

Alexandre Linhares

We present a formal verification of Wolstenholme's theorem -- $\left(\genfrac{}{}{0ex}{}{2p}{p}\right)\equiv 2(\mathrm{mod}{p}^3)$ for prime $p\ge 5$ -- in Lean~4 with Mathlib. The proof proceeds by expanding th…