Genuine AI-assisted solutions to Erdős problems begin: #124 (Aristotle), #1026 (48-hour human–AI collaboration)
In Nov–Dec 2025 AI tools produced the first genuinely new (if modest) solutions to Erdős problems. Harmonic's Aristotle proved a version of #124 in Lean autonomously (29 Nov). Erdős #1026 (posed 1975) was fully solved within ~48 hours by humans combining Aristotle, AlphaEvolve, GPT and deep-research tools (7–9 Dec). Terence Tao warned these were 'long-tail' problems.
Key facts
- #124 (from a 1995 paper): Aristotle proved it autonomously in Lean from the formal statement; Bloom noted it was the easier of two variants, and Tao's wiki lists it as partial
- #1026: Aristotle proved the key case c(k²)=1/k in Lean (7 Dec); full answer c(k²+2a+1) = k/(k²+a) assembled by 8–9 Dec
- Tao on #1026: 'It was only through the combined efforts of all the contributors and their tools that all these key inputs were able to be assembled within 48 hours.'
- #367: partial result by Alexeev, van Doorn and Tao with Aristotle and Gemini Deep Think (Nov 2025)
- #707 ($1000 problem): Alexeev & Mixon disproved it with ChatGPT-assisted Lean checks, then found Marshall Hall Jr. had a counterexample in 1947
- Tao: such results 'do not meet the hyped up goal of AI autonomously solving major mathematical open problems'
Science result
- Field
- mathematics / combinatorics / number theory
- Problem
- Erdős problems #124, #367, #707, #1026 and others (open since 1975)
- Result
- First AI-involved genuine new solutions of listed-open Erdős problems, including a full solution of #1026 and a Lean-verified autonomous proof for a variant of #124.
- AI system
- Aristotle, AlphaEvolve, Gemini Deep Think, GPT-5
- Human role
- Mixed: #124 near-autonomous (formal statement given); #1026 human–AI collaboration
- Verification
- Formal proofs in Lean for key steps; expert-checked (Tao, Bloom)
- Status
- confirmed
- Why surprising
- Problems open for decades fell in days, but experts stressed they were obscure ones that few people had seriously attempted.
What happened
After the October 2025 fiasco, a distributed community of mathematicians and amateurs began systematically attacking the ~1,100 Erdős problems with AI tools, with results logged on Tao's wiki. The first genuinely new results arrived within weeks.
Why it matters
Erdős problems became the first large, public, verifiable scoreboard for AI in research mathematics, and set the stage for 2026's much larger results.
Changelog
- 2026-09-29: created
Related events
- OpenAI researchers claim GPT-5 'solved' 10 Erdős problems; the solutions were already in the literature ★★★
- Erdős problem #728 solved near-autonomously by GPT-5.2 Pro and Harmonic's Aristotle, with a Lean proof ★★★★
Sources (5)
- discussionTerence Tao's wiki: AI contributions to Erdős problems
- discussionTerence Tao: The story of Erdős problem #1026
- discussionerdosproblems.com forum: problem #124
- discussionXena Project: formalization of Erdős problems
- paperAlexeev & Mixon on Erdős #707 (arXiv 2510.19804)
id: 2025-12-08-ai-erdos-problems-wave-late-2025 · updated 2026-09-29 · open in the interactive timeline