---
id: "2025-12-08-ai-erdos-problems-wave-late-2025"
url: "https://postcutoff.com/e/2025-12-08-ai-erdos-problems-wave-late-2025/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2025-12-08"
date_precision: day
category: science
importance: 4
confidence: medium
status: [Result confirmed]
verification: Lean-verified
sources: 5
editor: human editor
human_review: null
version: "2026-10-04"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2025-12-08-ai-erdos-problems-wave-late-2025/

# Genuine AI-assisted solutions to Erdős problems begin

Full title: 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'

## 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.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): in its training data
- Claude Opus 5.5 (training cutoff June 2026): in its training data
- Gemini 4 Hydrogen (training cutoff March 2026): in its training data
- Grok 4.7 (training cutoff May 2026): in its training data

## Sources

1. [Alexeev & Mixon on Erdős #707 (arXiv 2510.19804)](https://arxiv.org/abs/2510.19804) (arxiv.org, paper)
2. [Terence Tao's wiki: AI contributions to Erdős problems](https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems) (github.com, discussion)
3. [Terence Tao: The story of Erdős problem #1026](https://terrytao.wordpress.com/2025/12/08/the-story-of-erdos-problem-126/) (terrytao.wordpress.com, discussion)
4. [erdosproblems.com forum: problem #124](https://www.erdosproblems.com/forum/thread/124) (erdosproblems.com, discussion)
5. [Xena Project: formalization of Erdős problems](https://xenaproject.wordpress.com/2025/12/05/formalization-of-erdos-problems/) (xenaproject.wordpress.com, discussion)

## Changes

- 2026-09-29 (filed): Created

## Related

- 2026-01-06: [Erdős problem #728 solved near-autonomously by GPT-5.2 Pro and Harmonic's Aristotle, with a Lean proof](https://postcutoff.com/e/2026-01-06-erdos-728-gpt-5-2-aristotle/index.md)
- 2025-10-17: [OpenAI researchers claim GPT-5 'solved' 10 Erdős problems](https://postcutoff.com/e/2025-10-17-gpt-5-erdos-problems-controversy/index.md)
- People: [Terence Tao](https://postcutoff.com/person/terence-tao/)