AI and Terence Tao Close Out the 68-Year-Old Sendov Conjecture — Solving a Hidden Stronger Result Along the Way

Forum topic · 小凯 · 2026-08-19

Summary

In August 2026, Lech Mazur, founder of ProofAtlas, completed a proof of Sendov's conjecture with assistance from GPT-5.6 Pro, backed by roughly 90,000 lines of Lean 4 formalization code. Days later, Fields Medalist Terence Tao digested and simplified the proof, compressing it to about 15,000 lines of Lean code, and discovered the argument actually proves a stronger statement: the 1972 Phelps-Rodriguez conjecture, which demands strict inequality (|w − a| < 1). Sendov's conjecture, posed around 1958, states that for a complex polynomial with all zeros in the unit disk, each zero lies within distance 1 of a critical point. Tao described the proof as surprisingly elementary, relying mainly on Möbius transformations and a special case of Maclaurin's inequalities, verified entirely by Lean's type checker. The case highlights a new human-AI collaboration paradigm in mathematics, with formal verification as the trust foundation. Formalized code is open-sourced on GitHub.

In early August 2026, Lech Mazur, founder of the startup ProofAtlas, completed a proof of Sendov's conjecture with the help 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 (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, he found that the reorganized argument actually proves a stronger proposition, settling the 1972 Phelps-Rodriguez conjecture as a byproduct. One of the most famous open problems in complex analysis was thus closed once and for all, with AI playing a central role.

1. Sendov's Conjecture: An Elegantly Frustrating Problem

Sendov's conjecture was proposed around 1958 by the Bulgarian mathematician Blagovest Sendov, with a remarkably simple 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 each root have a critical point within distance 1?

The conjecture's 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 extreme example p(z) = zⁿ − 1 has roots at the n-th roots of unity and a unique critical point at the origin (with 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 n < 6 | | 1991 | Brown advanced to n < 7 | | 1996 | Borcea advanced to n < 8 | | 1999 | Brown and Xiang advanced to n < 9 — no low-degree progress for the next 20+ years | | 2020 | Terence Tao proved the case "n sufficiently large" (without an explicit bound), published in *Acta Mathematica* | | Early 2026 | Teng Zhang made Tao's "sufficiently large" explicit, up to n as high as 10²⁰⁰⁰⁰⁰ | | August 5, 2026 | Lech Mazur produced a proof using GPT-5.6 Pro, with 90,000 lines of Lean 4 code | | August 12, 2026 | Tao digested and simplified the proof to 15,000 lines of Lean code, finding that the Phelps-Rodriguez conjecture follows |

The mathematician who posed the conjecture — himself a PhD student at the time — failed to crack it for 17 years; it was finally resolved 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 was fully carried through under open peer-review-style scrutiny.

3. Why Phelps-Rodriguez Is a Stronger Statement

Tao's digested argument actually proves what is called 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 such that |w − a| < 1.

This directly implies the Phelps-Rodriguez conjecture (1972), which requires the distance to be strictly less than 1, except when a lies on the unit circle and p is a scalar multiple of zⁿ − aⁿ. Where Sendov asked "is distance ≤ 1 enough?", the digested proof delivers "distance < 1 holds almost always" — stronger, finer, and still tight for the historical extremal examples.

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 required is merely a special case of Maclaurin's inequalities."

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 "distance greater than 1" condition 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 in-disk conditions on the point sets to derive a contradiction — here the polynomial p itself does not appear. 4. Branch analysis: the polarization identity plus Möbius transformation estimates give a key integral lower bound; this is the only place where a must be real.

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