arxiv: 2604.16507 · v1 · submitted 2026-04-14 · 💻 cs.LO

Recognition: unknown

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

Alexandre Linhares

Authors on Pith no claims yet

Pith reviewed 2026-05-10 13:38 UTC · model grok-4.3

classification 💻 cs.LO

keywords Wolstenholme theoremformal proofLean 4binomial coefficientmodular congruenceprime numberssymmetric polynomialspower sums

0 comments

The pith

A Lean 4 formalization proves that the central binomial coefficient equals 2 modulo p cubed for primes five and larger.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper provides a complete formal proof in Lean 4 of Wolstenholme's theorem, which states that for any prime number p at least 5, the binomial coefficient of 2p choose p is congruent to 2 modulo p to the third power. The authors achieve this through a series of nine lemmas that expand a product involving p and show specific divisibility properties using modular arithmetic. A reader might care because this removes any possibility of human error in the proof steps, confirming the theorem through rigorous machine checking in an interactive theorem prover.

Core claim

Wolstenholme's theorem asserts that binom(2p, p) ≡ 2 mod p^3 for prime p ≥ 5. The formal proof expands the shifted factorial product from k equals 1 to p minus 1 of p plus k to second order in p. It identifies the quadratic coefficient as the second elementary symmetric product and demonstrates its divisibility by p through the vanishing of power sums in the integers modulo p.

What carries the argument

The second-order expansion in p of the product ∏(p + k) for k from 1 to p-1, where the quadratic term's divisibility by p is established using power sum vanishing over the finite field Z/pZ.

Load-bearing premise

The library definitions for binomials and factorials in Lean 4 correspond exactly to the mathematical concepts, allowing the algebraic manipulations to hold as intended.

What would settle it

Finding a prime p where computing binom(2p,p) modulo p^3 yields a value other than 2, or locating an unaccounted case in the Lean code that violates the theorem statement.

read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is a complete Lean 4 formalization of a classical theorem via a clean algebraic expansion, but the missing source code blocks any real check on the encodings.

read the letter

The paper delivers the first reported Lean 4 proof of Wolstenholme's theorem, that central binomial coefficient congruence modulo p cubed for primes at least 5. The route goes through a second-order expansion of the shifted factorial product, ties the quadratic term to the second elementary symmetric polynomial in the reciprocals, and uses power-sum vanishing modulo p to get the required divisibility. That algebraic framing is the main new piece here, and the development is reported as nine lemmas totaling roughly 800 lines with no sorrys at all. On the face of it, that is a solid, self-contained formalization that avoids the usual combinatorial detours in these proofs.

Referee Report

1 major / 0 minor

Summary. The manuscript presents a formal verification of Wolstenholme's theorem asserting that binom(2p,p) ≡ 2 mod p^3 for prime p ≥ 5, realized in Lean 4 with Mathlib. The proof expands the shifted factorial product ∏_{k=1}^{p-1}(p+k) to second order in p, identifies the quadratic coefficient as the second elementary symmetric function of the reciprocals, and establishes its p-divisibility via vanishing of power sums in Z/pZ. The development is stated to comprise nine lemmas in approximately 800 lines with zero sorry declarations and is claimed to be the first such verification in Lean 4, obtained via collaboration between a relational analogy engine and human formalization.

Significance. A machine-checked proof of this classical congruence, with explicit zero-sorry status and reliance on standard Mathlib components for binomial coefficients and modular arithmetic, would constitute a useful addition to the corpus of formally verified number theory. The absence of ad-hoc axioms or invented entities in the reported development further supports its potential reliability as a benchmark for AI-assisted theorem proving.

major comments (1)

[Abstract] Abstract and proof sketch: the central claim of a complete, machine-checked formalization (nine lemmas, ~800 lines, zero sorry) cannot be assessed because the Lean 4 source code is neither included nor linked via a public repository. This blocks verification that the encoding of binom(2p,p), the product expansion inside Z or Z/p^3Z, the correct introduction of inverses for 1..p-1, and the passage from rational symmetric sums to the integer congruence mod p^3 introduce no hidden divisibility conditions, all of which are load-bearing for the stated result.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful review, positive assessment of the work's significance, and recommendation. We address the single major comment below.

read point-by-point responses

Referee: [Abstract] Abstract and proof sketch: the central claim of a complete, machine-checked formalization (nine lemmas, ~800 lines, zero sorry) cannot be assessed because the Lean 4 source code is neither included nor linked via a public repository. This blocks verification that the encoding of binom(2p,p), the product expansion inside Z or Z/p^3Z, the correct introduction of inverses for 1..p-1, and the passage from rational symmetric sums to the integer congruence mod p^3 introduce no hidden divisibility conditions, all of which are load-bearing for the stated result.

Authors: We agree that the absence of the Lean 4 source code or a public repository link prevents independent verification of the implementation details. The manuscript reports a development of nine lemmas in ~800 lines with zero sorry declarations, but does not provide the code. To address this, we will add an explicit link to a public GitHub repository containing the full formalization in the revised manuscript (both in the abstract and a new dedicated section). The repository will include the Mathlib-based definitions of binom(2p,p), the second-order expansion of the shifted product inside Z or Z/p^3Z, the handling of inverses for 1..p-1, the identification of the quadratic coefficient with the second elementary symmetric function, and the use of vanishing power sums in Z/pZ to establish p-divisibility. This will allow direct inspection of all load-bearing steps and confirm the absence of hidden divisibility assumptions. We will also expand the abstract's proof sketch to map each high-level step to the corresponding lemma names. revision: yes

Circularity Check

0 steps flagged

No circularity: derivation is self-contained formalization from definitions

full rationale

The paper's derivation chain consists of nine lemmas that expand the binomial coefficient definition via the shifted product ∏_{k=1}^{p-1}(p+k), identify the quadratic term with the second elementary symmetric function, and invoke standard power-sum vanishing in ℤ/pℤ to establish divisibility by p. These steps rely on Mathlib encodings of factorials, binomial coefficients, and modular arithmetic together with explicit polynomial identities; no fitted parameters, self-referential definitions, or load-bearing self-citations are present. The mention of an analogy engine pertains only to discovery and does not substitute for the machine-checked lemmas. The formalization is therefore independent of its own outputs and reduces directly to the stated mathematical objects and standard results.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The proof rests on standard mathematical definitions and lemmas already present in Mathlib, including the binomial theorem, properties of elementary symmetric polynomials, and the vanishing of certain power sums in finite fields. No free parameters are introduced or fitted, and no new mathematical entities are postulated.

axioms (2)

standard math Binomial coefficient equals the ratio of falling factorials or the product form used in the expansion
Invoked when relating the binomial to the shifted product prod (p+k).
standard math Power sums of nonzero residues vanish modulo p for exponents 1 to p-2
Used to establish that the second elementary symmetric sum is divisible by p.

pith-pipeline@v0.9.0 · 5447 in / 1457 out tokens · 64253 ms · 2026-05-10T13:38:31.584940+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

41 extracted references · 7 canonical work pages · 3 internal anchors

[1]

On certain properties of prime numbers,

J. Wolstenholme, “On certain properties of prime numbers,”Quarterly Journal of Pure and Applied Mathematics, vol. 5, pp. 35–39, 1862
[2]

Mathlib: A unified library of mathematics formalized in Lean,

The Mathlib Community, “Mathlib: A unified library of mathematics formalized in Lean,” https://leanprover-community.github.io/mathlib4_docs/, 2024

2024
[3]

The square of the Fermat quotient,

A. Granville, “The square of the Fermat quotient,”Integers: Electronic Journal of Combina- torial Number Theory, vol. 4, A22, 2004

2004
[4]

On the Measure of Intelligence

F. Chollet, “On the measure of intelligence,”arXiv preprint arXiv:1911.01547, 2019

work page internal anchor Pith review arXiv 1911
[5]

D. R. Hofstadter and the Fluid Analogies Research Group,Fluid Concepts & Creative Analo- gies: Computer Models of the Fundamental Mechanisms of Thought. New York: Basic Books, 1995

1995
[6]

D. R. Hofstadter,G¨ odel, Escher, Bach: An Eternal Golden Braid, 20th anniversary ed. New York: Basic Books, 1999

1999
[7]

D. R. Hofstadter and E. Sander,Surfaces and Essences: Analogy as the Fuel and Fire of Thinking. New York: Basic Books, 2013

2013
[8]

The Copycat Project,

D. Hofstadter, “The Copycat Project,” MIT AI Lab, Tech. Rep., Jan. 1984

1984
[9]

Mitchell,Analogy-Making as Perception: A Computer Model

M. Mitchell,Analogy-Making as Perception: A Computer Model. Cambridge, MA: The MIT Press, 1993. 9

1993
[10]

The emergence of understanding in a computer model of concepts and analogy-making,

M. Mitchell and D. R. Hofstadter, “The emergence of understanding in a computer model of concepts and analogy-making,”Physica D: Nonlinear Phenomena, vol. 42, no. 1–3, pp. 322– 334, 1990

1990
[11]

High-level perception, representation, and analogy: A critique of artificial intelligence methodology,

D. J. Chalmers, R. M. French, and D. R. Hofstadter, “High-level perception, representation, and analogy: A critique of artificial intelligence methodology,”Journal of Experimental & Theoretical Artificial Intelligence, vol. 4, no. 3, pp. 185–211, 1992

1992
[12]

Tabletop: An emergent, stochastic model of analogy- making,

R. M. French and D. Hofstadter, “Tabletop: An emergent, stochastic model of analogy- making,” inProceedings of the 13th Annual Cognitive Science Society Conference. Lawrence Erlbaum Associates, 1991

1991
[13]

PHAEACO: A cognitive architecture inspired by Bongard’s problems,

H. E. Foundalis, “PHAEACO: A cognitive architecture inspired by Bongard’s problems,” Ph.D. thesis, Indiana University, 2006

2006
[14]

Letter Spirit (Part Two): Modeling creativity in a visual domain,

J. Rehling, “Letter Spirit (Part Two): Modeling creativity in a visual domain,” Ph.D. thesis, Indiana University, 2001

2001
[15]

MUSICAT: A computer model of musical listening and analogy-making,

E. P. Nichols, “MUSICAT: A computer model of musical listening and analogy-making,” Ph.D. thesis, Indiana University, 2012

2012
[16]

An active symbols theory of chess intuition,

A. Linhares, “An active symbols theory of chess intuition,”Minds and Machines, vol. 15, pp. 131–151, 2005

2005
[17]

Understanding our understanding of strategic scenarios: What role do chunks play?

A. Linhares and P. Brum, “Understanding our understanding of strategic scenarios: What role do chunks play?”Cognitive Science, vol. 31, no. 6, pp. 989–1007, 2007

2007
[18]

Questioning Chase and Simon’s (1973) ‘Perception in Chess’: The ‘experience recognition’ hypothesis,

A. Linhares and A. E. T. A. Freitas, “Questioning Chase and Simon’s (1973) ‘Perception in Chess’: The ‘experience recognition’ hypothesis,”New Ideas in Psychology, vol. 28, no. 1, pp. 64–78, 2010

1973
[19]

Entanglement of perception and reasoning in the combinatorial game of chess: Differential errors of strategic reconstruction,

A. Linhares, A. E. T. A. Freitas, A. Mendes, and J. S. Silva, “Entanglement of perception and reasoning in the combinatorial game of chess: Differential errors of strategic reconstruction,” Cognitive Systems Research, vol. 13, no. 1, pp. 72–86, 2012

2012
[20]

What is the nature of the mind’s pattern-recognition process?

A. Linhares and D. M. Chada, “What is the nature of the mind’s pattern-recognition process?” New Ideas in Psychology, vol. 31, no. 2, pp. 108–121, 2013

2013
[21]

The emergence of choice: Decision-making and strategic thinking through analo- gies,

A. Linhares, “The emergence of choice: Decision-making and strategic thinking through analo- gies,”Information Sciences, vol. 259, pp. 36–56, 2014

2014
[22]

Deep Vision: Seeing the essence of proofs through relational analogy,

A. Linhares, “Deep Vision: Seeing the essence of proofs through relational analogy,” ARGO LABS Internal Report
[23]

Deep Vision,

A. Linhares, “Deep Vision,” ARGO LABS Internal Report
[24]

Meštrović,Wolstenholme’s Theorem: Its Generalizations and Extensions in the Last Hundred and Fifty Years, Preprint arXiv:1111.3057 (2011)

R. Meˇ strovi´ c, “Wolstenholme’s theorem: Its generalizations and extensions in the last hundred and fifty years (1862–2012),”arXiv preprint arXiv:1111.3057, 2011

work page arXiv 2012
[25]

On the converse of Wolstenholme’s theorem,

R. J. McIntosh, “On the converse of Wolstenholme’s theorem,”Acta Arithmetica, vol. 71, no. 4, pp. 381–389, 1995

1995
[26]

Congruences for Wolstenholme primes,

R. Meˇ strovi´ c, “Congruences for Wolstenholme primes,”Czechoslovak Mathematical Journal, vol. 65, no. 1, pp. 237–253, 2015. 10

2015
[27]

Super congruences and Euler numbers,

Z.-W. Sun, “Super congruences and Euler numbers,”Science China Mathematics, vol. 54, no. 12, pp. 2509–2535, 2011

2011
[28]

Open conjectures on congruences,

Z.-W. Sun, “Open conjectures on congruences,”Nanjing University Journal of Mathematical Biquarterly, vol. 36, no. 1, pp. 1–99, 2019

2019
[29]

Wolstenholme revisited,

I. M. Gessel, “Wolstenholme revisited,”American Mathematical Monthly, vol. 115, no. 5, pp. 458–461, 2008

2008
[30]

On Wolstenholme’s theorem and its converse,

C. Helou and G. Terjanian, “On Wolstenholme’s theorem and its converse,”Journal of Number Theory, vol. 128, no. 3, pp. 475–499, 2008

2008
[31]

Power sums of polynomials over finite fields and applications: A survey,

D. S. Thakur, “Power sums of polynomials over finite fields and applications: A survey,”Finite Fields and Their Applications, vol. 32, pp. 171–191, 2015

2015
[32]

A proof of Wolstenholme's theorem and congruence properties via an Egorychev-type integral

J.-C. Pain, “A proof of Wolstenholme’s theorem and congruence properties via an Egorychev- type integral,”arXiv preprint arXiv:2604.03000, 2026

work page internal anchor Pith review Pith/arXiv arXiv 2026
[33]

Reciprocal sums as a knowledge metric: Theory, computation, and perfect numbers,

J. Bayless and D. Klyve, “Reciprocal sums as a knowledge metric: Theory, computation, and perfect numbers,”American Mathematical Monthly, vol. 120, no. 9, pp. 822–831, 2013

2013
[34]

Thep-adic growth of harmonic sums,

K. Conrad, “Thep-adic growth of harmonic sums,” Expository note, University of Connecticut, 2020

2020
[35]

Some congruences involving binomial coefficients and Fermat quotients,

W.-W. Qi, “Some congruences involving binomial coefficients and Fermat quotients,”arXiv preprint arXiv:2512.01385, 2025

work page arXiv 2025
[36]

The congruence of Wolstenholme and generalized binomial coefficients related to Lucas sequences,

E. Trevi˜ no, “The congruence of Wolstenholme and generalized binomial coefficients related to Lucas sequences,”arXiv preprint arXiv:1409.8629, 2014

work page arXiv 2014
[37]

Proofs of power sum and binomial coefficient congruences via Pascal’s identity,

K. Davis, “Proofs of power sum and binomial coefficient congruences via Pascal’s identity,” American Mathematical Monthly, vol. 115, no. 6, pp. 549–551, 2008

2008
[38]

A complete formalization of Fermat’s Last Theorem for regular primes in Lean,

R. Brasca, C. Birkbeck, E. Rodriguez Boidi, A. Best, R. Van De Velde, and A. Yang, “A complete formalization of Fermat’s Last Theorem for regular primes in Lean,”Annals of For- malized Mathematics, vol. 1, 2025

2025
[39]

Joseph Tooby-Smith

P. Song, K. Yang, and A. Anandkumar, “Lean Copilot: Large language models as copilots for theorem proving in Lean,”arXiv preprint arXiv:2404.12534, 2024

work page arXiv 2024
[40]

AlphaProof: AI system for formal mathematical rea- soning at the IMO level,

AlphaProof Team (Google DeepMind), “AlphaProof: AI system for formal mathematical rea- soning at the IMO level,” 2025

2025
[41]

Aristotle: IMO-level Automated Theorem Proving

The Harmonic Team, “Aristotle: IMO-level automated theorem proving,”arXiv preprint arXiv:2510.01346, 2025. 11

work page internal anchor Pith review arXiv 2025