In January 2026, something unprecedented happened in mathematics. Three problems from the legendary Erdős Problem List — unsolved for decades — fell in just seven days. The proofs were generated by GPT-5.2 Pro, formalized in Lean 4 by Harmonic's Aristotle system, and verified by Fields Medalist Terence Tao himself.
This is the story of Problem #397 — and why it matters.
The Problem: Erdős #397 (1975)
In 1975, Paul Erdős, Ronald Graham, András Ruzsa, and Endre Strauss posed a deceptively simple question about central binomial coefficients — the numbers C(2n, n) = (2n)! / (n!)² that appear in Pascal's triangle, probability theory, and combinatorics.
The Conjecture: Are there only finitely many solutions to the equation
C(2m₁, m₁) · C(2m₂, m₂) · ... = C(2n₁, n₁) · C(2n₂, n₂) · ...
where all the mi and nj are distinct positive integers?
In plain language: can you find two different sets of distinct integers whose products of central binomial coefficients are exactly equal? Erdős conjectured this could only happen finitely many times.
For 50 years, nobody could prove or disprove it.
The Disproof: An Infinite Family of Counterexamples
On January 11, 2026, Neel Somani prompted GPT-5.2 Pro to examine the conjecture. After approximately 15 minutes of reasoning, the AI generated a complete disproof by constructing an infinite family of counterexamples.
The Construction: For any integer a ≥ 2, define c = 8a² + 8a + 1. Then:
C(2a, a) · C(4a+4, 2a+2) · C(2c, c) = C(2a+2, a+1) · C(4a, 2a) · C(2c+2, c+1)
This is not one counterexample — it is an infinite parametric family. Every value of a ≥ 2 produces a distinct solution where two products of central binomial coefficients with completely different indices are exactly equal. The conjecture is false.
A Concrete Example: a = 2
Plugging in a = 2 gives c = 8(4) + 8(2) + 1 = 49. The equation becomes:
| Left side | C(4, 2) · C(12, 6) · C(98, 49) = 6 · 924 · 49,699,896,378,196,... |
| Right side | C(6, 3) · C(8, 4) · C(100, 50) = 20 · 70 · 100,891,344,545,564,... |
Both sides evaluate to the same enormous number — proving Erdős wrong on this conjecture.
The Verification Pipeline
What makes this result bulletproof is the verification chain:
- Step 1 — AI Generation: GPT-5.2 Pro generated the informal proof and the parametric construction
- Step 2 — Formalization: Harmonic's Aristotle system auto-translated the proof into Lean 4 code — a formal verification language where every logical step must be explicit and machine-checkable
- Step 3 — Human Verification: Fields Medalist Terence Tao reviewed and accepted the proof within one day
- Status: erdosproblems.com now marks Problem #397 as "DISPROVED (LEAN)"
Three Problems in Seven Days
Problem #397 was not an isolated event. It was the climax of an extraordinary week:
| Jan 4-8 | Problem #728 (factorial divisibility) — solved by Kevin Barreto & AcerFur using GPT-5.2 Pro. arXiv writeup available. |
| Jan 8-10 | Problem #729 (factorial divisibility, ignoring small primes) — closely related to #728, formalized in Lean |
| Jan 11 | Problem #397 (products of central binomial coefficients) — disproved by Neel Somani using GPT-5.2 Pro |
All three were verified by Terence Tao. All three were formalized in Lean 4.
Tao's Perspective: Important Caveats
Terence Tao, while acknowledging the achievement, offered important context on Mathstodon:
- These problems were "lowest-hanging fruit" — solvable with standard, established techniques that hadn't been applied to these specific formulations
- The arguments are original (not previously published) but use known methods — the AI's contribution was applying existing techniques, not inventing new mathematics
- His primary interest is "the emerging AI-powered capability to rapidly write and rewrite expositions" — the ability to formalize proofs automatically may be more impactful than the solutions themselves
In other words: the AI didn't achieve a creative breakthrough comparable to human mathematical insight. It achieved something different and arguably more disruptive — it made the search-and-verify loop fast enough to clear a backlog of open problems that humans simply hadn't gotten around to.
Why This Matters Beyond Mathematics
The Erdős Problem List contains over 1,000 unsolved problems. If AI can clear the "standard technique" backlog — perhaps hundreds of these problems — it fundamentally changes the research landscape:
- For mathematicians: The tedious "check if known methods work" phase can be automated, freeing human creativity for genuinely hard problems
- For AI: Lean formalization provides a ground truth verification system — unlike natural language, you cannot hallucinate a valid Lean proof
- For science broadly: If AI can discover and verify mathematical truths autonomously, the same pipeline applies to protein folding, drug design, and materials science
We are entering the era of machine-verifiable discovery. The AI proposes, the proof assistant disposes. No ambiguity, no hallucination — just mathematics.
Sources: Erdős Problems #397, Neel Somani (X), Terence Tao (Mathstodon), arXiv: Problem #728 Lean Proof, The Neuron Daily