AI + Terence Tao Close Out Sendov's Conjecture After 68 Years — And Solve a Hidden Stronger Result Along the Way

Forum topic · 小凯 · 2026-08-19

Summary

In early August 2026, Lech Mazur, founder of the startup ProofAtlas, completed a proof of Sendov's Conjecture with the assistance of GPT-5.6 Pro, accompanied by roughly 90,000 lines of Lean 4 formalization code. On August 12, Fields Medalist Terence Tao published a blog post explaining that, also with substantial AI assistance, he had digested, simplified, and re-formalized the proof, compressing the Lean code to about 15,000 lines. More importantly, Tao found that the streamlined argument actually proves a stronger statement, resolving the 1972 Phelps-Rodriguez Conjecture as a corollary. The article reviews the conjecture's statement (a local counterpart of the Gauss-Lucas theorem), traces 68 years of incremental progress, outlines the surprisingly elementary proof strategy via contradiction, normalization, centroid identities, and Bernstein polynomial certificates checked in Lean, and discusses the emerging human-AI collaboration paradigm in formal mathematics. The formalized code is open-sourced at github.com/teorth/sendov.

In early August 2026, Lech Mazur, founder of the startup ProofAtlas, completed a proof of Sendov's Conjecture with the assistance of GPT-5.6 Pro, accompanied by roughly 90,000 lines of Lean 4 formalization code. On August 12, Fields Medalist Terence Tao published a blog post explaining that, over several days and also with heavy AI assistance, he had digested, simplified, and re-formalized the proof, compressing the Lean code to about 15,000 lines. Crucially, he found that the streamlined argument actually proves a stronger statement, and the 1972 Phelps-Rodriguez Conjecture falls as a corollary. One of the most famous open problems in complex analysis has been closed out — with AI in the loop.

1. Sendov's Conjecture: An Elegantly Frustrating Problem

Sendov's Conjecture was proposed around 1958 by the Bulgarian mathematician Blagovest Sendov, with a minimal statement:

> Let p(z) be a complex polynomial of degree n (n ≥ 2) whose zeros all lie in the closed unit disk (i.e., |z| ≤ 1). Then for any zero a of p, there exists at least one critical point w (a zero of the derivative p'(z)) such that |w − a| ≤ 1.

In other words: if all roots of a complex polynomial lie in the unit disk, must there always be a critical point within distance 1 of each root?

The background is the classical Gauss-Lucas theorem: all critical points of a polynomial lie in the convex hull of its zeros — a global statement, whereas Sendov asks for a local version.

The extremal example p(z) = zⁿ − 1 has roots at the unit roots and a unique critical point at the origin (multiplicity n−1), at distance exactly 1. This shows the constant 1 is tight — it cannot be improved.

2. A 68-Year Relay

| Year | Progress | |---|---| | 1969 | Meir and Sharma proved the case n < 6 | | 1991 | Brown pushed to n < 7 | | 1996 | Borcea pushed to n < 8 | | 1999 | Brown and Xiang pushed to n < 9 — then no low-degree progress for over 20 years | | 2020 | Tao proved the case of "n sufficiently large" (with no explicit bound), published in *Acta Mathematica* | | Early 2026 | Teng Zhang made Tao's "sufficiently large" explicit, up to n as large as 10²⁰⁰⁰⁰⁰ | | Aug 5, 2026 | Lech Mazur produced a proof using GPT-5.6 Pro, with 90,000 lines of Lean 4 code | | Aug 12, 2026 | Tao digested and simplified the proof to 15,000 lines of Lean code, discovering that the Phelps-Rodriguez Conjecture follows |

The mathematician who posed the conjecture — then a PhD student — spent 17 years without breaking through; the key proof was ultimately completed by a human-AI combination. This is one of the few cases in mathematical history where an AI-assisted resolution of a long-standing classical problem ran the full course under public peer-review-style scrutiny.

3. Why Phelps-Rodriguez Is a Stronger Statement

Tao's digested argument actually proves "Conjecture 3" (the interior form of Sendov):

> Let n ≥ 2 and let p be a degree-n polynomial with all zeros in the unit disk. If a is a zero of p, then there exists a critical point w of p with |w − a| < 1.

This directly implies the Phelps-Rodriguez Conjecture (1972): the distance can be taken strictly less than 1, except when a lies on the unit circle and p is a scalar multiple of zⁿ − aⁿ. In other words, where Sendov asked 68 years ago whether "distance ≤ 1" suffices, the digested proof directly shows "distance < 1 almost always works" — stronger, finer, and still tight for the historical extremal example.

4. A "Surprisingly Elementary" Proof

Tao spoke highly of the proof: "The proof is surprisingly elementary — apart from the fundamental theorem of algebra and basic properties of Möbius transformations, almost no tools from complex analysis are used; the deepest inequality needed is a special case of Maclaurin's inequality."

The skeleton is a four-step proof by contradiction:

1. Normalization: rotate the hypothetical counterexample so the zero a lies in 0, 1); replace the critical points wⱼ with reciprocal coordinates qⱼ = 1/(a − wⱼ), translating the counterexample condition "distance greater than 1" into two point sets inside the unit disk (the remaining zeros and the reciprocal critical points). 2. Commutation identities: by evaluating p and p′ at natural points, derive four algebraic relations — a centroid identity, a polarization identity, and two origin identities — linking the centroids of the zero set and the critical point set. 3. Eliminating the polynomial: combine the four identities with the unit-disk conditions to derive a contradiction — the polynomial p itself never appears at this stage. 4. Case analysis: the polarization identity plus Möbius transformation estimates yield a key integral lower bound; this is the only place where a must be real.

For low degrees (n ≤ 5), term-by-term analysis of the integral yields a contradiction directly. For higher degrees (n ≥ 5), two inequalities — the polarization inequality (an AM-GM relaxation of the integral) and the origin inequality (from the first and second origin identities plus the centroid identity) — constrain the feasible region. For n ≥ 101 the two feasible regions are analytically disjoint; for 5 ≤ n ≤ 100, certificates built from Bernstein polynomials with exact rational arithmetic provide numerical verification, all checked by the Lean system.