A digestion of the proof of Sendov's conjecture
Terence Tao · blog · 2026-08-12 · ★★★★ · archived
Tao distils Lech Mazur's AI-generated proof of Sendov's conjecture (1958) into an elementary argument and a much shorter Lean formalisation.
Summary
Blog post by Terence Tao, 12 Aug 2026. It digests the proof of Sendov's conjecture, and the Phelps–Rodriguez strengthening for all n ≥ 2, that Lech Mazur obtained with an AI tool. Tao shows the argument needs essentially only Maclaurin's inequality. He did the digestion "with heavy AI assistance" and cut the Lean formalisation from about 90,000 to about 15,000 lines. He later submitted it to the new Palomar registry of Lean-verified results (18 Aug). It is a model case of human mathematicians turning an AI proof into understanding. Checked via WebFetch of the August 2026 archive.
Archived text
Page title: A digestion of the proof of Sendov’s conjecture
Page description: This post concerns the following conjecture of Sendov, as well as its strengthening by Phelps–Rodriguez: Conjecture 1 (Sendov’s conjecture) Let $latex {n \geq 2}&fg=000000$, and let…
Metadata archived 2026-09-29; see Summary for content.
Related events
All posts · id: 2026-08-12-tao-sendov-conjecture-digestion