Sendov Conjecture Closed After 67 Years: An AI-Assisted, Formally Verified Proof

*Note: This is a structured summary of the original Chinese forum post, which describes events presented as occurring in 2026.*

The conjecture

Proposed by Blagovest Sendov in Sofia, Bulgaria, in 1958 (sometimes called the Ilieff–Sendov conjecture in early literature):

> If all zeros of a complex polynomial P lie within a disk of diameter 2, then every zero is within distance 1 of some critical point (a zero of P').

The difficulty: a polynomial can have arbitrarily many zeros but only finitely many critical points, so each zero must be "assigned" a guardian from a limited pool.

Key points

• 1958–1980s: Low-degree cases (degree ≤ 8) were settled by elementary methods; Erdős and Chern took interest in 1979.
• 2020: Terence Tao announced a proof strategy establishing an absolute constant N such that the conjecture holds for all degrees ≥ N (published in *Acta Mathematica*, 2022). This reduced the problem to a finite—but potentially enormous—computation.
• 2026: Lech Mazur used an AI system (reportedly a hybrid of OpenAI and Anthropic models) to generate a candidate proof for the remaining finite cases, producing roughly 90,000 lines of Lean 4 code structured as an exhaustive case-search tree.

Human compression: 90,000 → 15,000 lines

Mazur and collaborators (including Tao as an independent verifier) rewrote the AI draft by:

1. Extracting geometric identities (barycenter, inversion at the origin) to merge hundreds of duplicated cases into single lemmas. 2. Applying Möbius transformations to normalize disk coordinates and reinterpret the distance-≤-1 condition symmetrically. 3. Introducing Maclaurin inequalities to clamp coefficient comparisons continuously, eliminating case-by-case enumeration.

| Stage | Lean lines | Note | | --- | ---: | --- | | AI draft | ~90,000 | exhaustive case tree | | Human-refined | ~15,000 | geometric + Möbius + Maclaurin framework | | Compression | ~6:1 | equivalent proof, restructured |

Lean's automatic kernel checking verified every lemma; sorry placeholders fell from ~4,200 in the AI draft to 11 after compression.

Tao's independent verification

In August, Tao announced end-to-end verification of the Lean proof: (1) regenerating an independent but structurally similar proof from the AI toolchain, (2) mapping key lemmas onto his 2020 analytic framework, and (3) analyzing error patterns—confirming the 11 remaining sorrys were trivially fillable syntactic gaps.

Byproducts and related problems

• Phelps-Rodriguez conjecture (allowing one exceptional zero outside the disk) was resolved as a light extension of the same framework.
• Rubinstein's 1994 theorem on critical point–zero distances received a new, more elementary proof via Maclaurin inequalities.
• The Borcea and Schmeisser conjectures may be partially reachable; Smale's 18th problem (higher-dimensional analogue) cannot be directly attacked—Möbius transformations have no higher-dimensional counterpart.

Takeaways

• Formal verification is becoming expected infrastructure for claims that "close major open problems."
• A new tripartite paradigm: machines enumerate, humans find structure and meaning, Lean referees—all three were essential here.
• The 6:1 "compression ratio" (AI draft → human rewrite) may become a proxy metric for genuine mathematical understanding.
• The decisive insight—Möbius + Maclaurin—came from human mathematical taste, not the AI. AI saved the typing; humans supplied the viewpoint.

> Sendov asked a seemingly obvious question at age 30. An AI eventually wrote the most tedious part of the answer—but the 67-year weight behind "obvious" is not something AI could, or should, carry.

*Originally written August 2026, on the reported acceptance of the Lean-formalized proof by the Annals of Mathematics.*