Sendov's 1958 conjecture on polynomial roots proved with GPT-5.6 Pro; Tao simplifies and formalises it
Lech Mazur posted a computer-assisted proof, generated with GPT-5.6 Pro, of Sendov's conjecture for all degrees: if every root of a polynomial lies in the closed unit disk, each root is within distance 1 of a critical point. Terence Tao called it 'remarkably elementary', simplified it, and used AI agents to shrink the Lean proof from ~90k to ~15k lines.
Key facts
- Conjecture from 1958; previously known for degree < 9 (Brown–Xiang) and for sufficiently large degree (Tao, 2020)
- Mazur's preprint 5 Aug 2026 (some lists say 3 Aug); Tao's digestion 12 Aug 2026
- Tao extended the method to the Phelps–Rodriguez conjecture
Science result
- Field
- mathematics / complex analysis / geometry of polynomials
- Problem
- Sendov's conjecture (open since 1958)
- Result
- Proof of Sendov's conjecture for all degrees, formally verified in Lean.
- AI system
- GPT-5.6 Pro
- Human role
- Human orchestrated (Mazur); Tao simplified and formalised with AI agents
- Verification
- Formal proof in Lean; expert-checked by Tao
- Status
- confirmed
- Why surprising
- A 68-year-old conjecture that Tao himself had only proved for large degrees fell to an elementary AI-found argument.
What happened
A non-academic used GPT-5.6 Pro to generate a computer-assisted proof covering the remaining degrees. Tao then digested it into a short argument based on the fundamental theorem of algebra and the Maclaurin inequality.
Why it matters
It is a classic, well-known conjecture closed by AI, with the leading expert on the problem verifying and formalising the result.
Changelog
- 2026-09-29: created
Related posts (1)
- A digestion of the proof of Sendov's conjecture Terence Tao · blog · 2026-08-12
Tao distils Lech Mazur's AI-generated proof of Sendov's conjecture (1958) into an elementary argument and a much shorter Lean formalisation.
Related events
- Neurosurgery resident uses GPT-5.6 Sol to prove Crouzeix's conjecture in a 16-hour autonomous run ★★★★
- HRT conjecture (1996) disproved: 12 time-frequency shifts of a Schwartz function are linearly dependent, found with ChatGPT-assisted guesswork ★★★
- Palomar launches: a registry of Lean-verified mathematics to curb misrepresented AI proof claims ★★★
Sources (2)
- discussionTerence Tao: A digestion of the proof of Sendov's conjecture
- paperLech Mazur: Sendov conjecture proof (PDF)
id: 2026-08-05-sendov-conjecture-proved · updated 2026-09-29 · open in the interactive timeline