Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911605441167360 |
|---|---|
| author | Linhares, Alexandre |
| author_facet | Linhares, Alexandre |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_16507 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4 Linhares, Alexandre Logic in Computer Science 11A07 (Primary) 68V15, 11B65, 68T01 (Secondary) F.4.1; I.2.3; G.2.1 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. |
| title | Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4 |
| topic | Logic in Computer Science 11A07 (Primary) 68V15, 11B65, 68T01 (Secondary) F.4.1; I.2.3; G.2.1 |
| url | https://arxiv.org/abs/2604.16507 |