AI Proves Sendov’s Conjecture and Reveals a Stronger Result, Says Tao

Sendov Conjecture

For a complex polynomial p(z) of degree n ≥ 2 whose zeros all lie in the closed unit disk (|z| ≤ 1), each zero a has at least one critical point w (a zero of p′) satisfying |w‑a| ≤ 1.

Equivalently, if all roots of a polynomial lie in the unit circle, every root is within distance 1 of a critical point.

Extremal example

For p(z)=zⁿ‑1 the zeros are the n‑th roots of unity and the unique critical point is the origin of multiplicity n‑1, giving distance exactly 1. This shows the constant 1 cannot be improved.

Historical progress

1969 – Meir and Sharma proved the conjecture for n < 6.

1991 – Brown extended it to n < 7.

1996 – Borcea extended it to n < 8.

1999 – Brown and Xiang extended it to n < 9; no further low‑degree progress for over 20 years.

2020 – Terence Tao proved the conjecture for sufficiently large n (Acta Mathematica) without an explicit bound.

Early 2026 – Teng Zhang made Tao’s bound explicit, up to 10^200000.

AI‑assisted proof

Lech Mazur announced a computer‑assisted proof titled “A Computer‑Assisted Proof of Sendov’s Conjecture”. The proof was generated with the assistance of GPT‑5.6 Pro and formalized in Lean 4, comprising roughly 90 000 lines of code (see the PDF link below).

Terence Tao later spent several days digesting, simplifying, and re‑formalizing the proof, reducing the Lean code to about 15 000 lines. The revised proof is open‑sourced on GitHub ( github.com/teorth/sendov).

Tao’s analysis showed that the argument actually proves the stronger 1972 Phelps‑Rodriguez conjecture, which requires the distance to be strictly less than 1 unless a lies on the unit circle and p is a scalar multiple of zⁿ‑aⁿ.

Proof strategy

Core assumption (proof by contradiction) : Assume a counterexample exists – a degree‑n polynomial p whose zeros lie in the unit disk, but some zero a has no critical point within distance 1.

Step 1 – Normalization : Rotate the plane so that a becomes a real number in [0,1). Replace each critical point w_j by the reciprocal coordinate q_j = 1/(a‑w_j). The “no critical point within distance 1” condition translates into a bound on the q_j’s, packaging the counterexample as two point sets inside the unit disk: the remaining zeros z_j and the reciprocal critical points q_j.

Step 2 – Communication identities : Four relations are derived by evaluating p and p′ at natural points: (i) centroid identity (centroids of zeros and critical points coincide), (ii) polarization identity, (iii) first origin identity, and (iv) second origin identity. These are called “communication identities”.

Step 3 – Elimination of the polynomial : Using the four identities together with the fact that both point sets lie in the unit disk, a contradiction is derived without the polynomial p appearing explicitly.

Step 4 – Branch‑point analysis : The polarization identity combined with a Möbius‑transform estimate yields a crucial integral lower bound (shown in the accompanying diagram). This is the only place where a is assumed real and it initiates the case split.

Low‑degree case (n ≤ 5) : Define the scalar X(t)=a+(1‑a²)t to control each term of the integrand. The resulting integral is strictly less than 1 for 0 < a < 1 and m ≤ 4, contradicting the lower bound.

High‑degree case (n ≥ 5) : Two inequalities are required.

Polarization inequality : Obtained by relaxing the integral via the AM‑GM inequality.

Origin inequality : Derived from the first and second origin identities together with the centroid identity.

These inequalities constrain the feasible region of the core parameters – the real part x of the average of the q_j’s and a rational‑function expression R(a) defined in the proof. For n ≥ 101 the two inequalities are analytically shown to be incompatible; for 5 ≤ n ≤ 100 the incompatibility is verified numerically using exact rational‑coefficient Bernstein‑polynomial certificates, all checked by Lean.

Boundary case (|a|=1) : Previously solved by Rubinstein. Tao reproduces it using the same framework, replacing the polarization identity with the Meir‑Sharma identity, which forces each q_j = 1 and consequently p must be a scalar multiple of zⁿ‑aⁿ – exactly the excluded extremal case in the Phelps‑Rodriguez conjecture.

The proof relies only on the fundamental theorem of algebra, basic properties of Möbius transformations, and the Maclaurin inequality (a special case of the arithmetic‑geometric‑harmonic mean inequality).

Stronger conjecture

The argument proves the Phelps‑Rodriguez conjecture (1972): for a polynomial with all zeros in the unit disk, the distance from any zero a to the nearest critical point is strictly less than 1, unless |a|=1 and p is a scalar multiple of zⁿ‑aⁿ.

References

Proof PDF: https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf

Terence Tao’s blog post: https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/

GitHub repository (Lean code): https://github.com/teorth/sendov