Erdős problem #728 solved near-autonomously by GPT-5.2 Pro and Harmonic's Aristotle, with a Lean proof
On 4–6 Jan 2026 amateur Kevin Barreto relayed an informal argument from GPT-5.2 Pro to Harmonic's Aristotle, which formalised it in Lean. It was widely accepted as the first Erdős problem solved essentially autonomously by AI with no prior solution in the literature. Terence Tao said the win 'says more about speed than difficulty'.
Key facts
- Jan 4: first run solved an ambiguous reading of the problem; Jan 5: GPT-5.2 Pro upgraded the argument to the intended statement; Jan 6: Aristotle formalised it
- Tao: 'a near-autonomous solution that has not been reproduced in existing literature'
- Human role: prompting and relaying only; Barreto clarified no mathematical hint was given
- Write-up: arXiv 2601.07421
Science result
- Field
- mathematics / number theory / combinatorics
- Problem
- Erdős problem #728
- Result
- Full solution of the intended version of #728, generated by GPT-5.2 Pro and machine-checked in Lean by Aristotle.
- AI system
- GPT-5.2 Pro, Aristotle
- Human role
- Near-autonomous: human relayed prompts between two AI systems
- Verification
- Formal proof in Lean; endorsed by Terence Tao
- Status
- confirmed
- Why surprising
- An end-to-end AI pipeline, informal proof plus formal verification, closed an Erdős problem with essentially no human mathematics.
What happened
An amateur used two commercial AI systems in tandem: one to find a proof and one to formally verify it. After fixing a misreading of the problem statement, the pipeline produced a Lean-checked solution.
Why it matters
It showed the combination of informal LLM reasoning with formal verification as a practical, trustworthy workflow for research maths that non-experts could run.
Changelog
- 2026-09-29: created
Related events
- Genuine AI-assisted solutions to Erdős problems begin: #124 (Aristotle), #1026 (48-hour human–AI collaboration) ★★★★
- Amateur with GPT-5.4 Pro 'vibe-maths' a 60-year-old Erdős conjecture on primitive sets; Tao co-authors the paper ★★★★
- DeepMind's Aletheia agent and Gemini Deep Think report autonomous Erdős solutions and new physics and CS results ★★★★
Sources (3)
- paperResolution of Erdős Problem #728: a writeup of Aristotle's Lean proof (arXiv 2601.07421)
- discussionTerence Tao's wiki: AI contributions to Erdős problems
- pressThe Decoder: Tao says GPT-5.2 Pro cracked an Erdős problem but warns the win says more about speed than difficulty
id: 2026-01-06-erdos-728-gpt-5-2-aristotle · updated 2026-09-29 · open in the interactive timeline