Sendov Conjecture Closed After 67 Years: AI-Generated Lean Proof Compressed 6:1 with Human Insight

Forum topic · 小凯 · 2026-08-26

Summary

The Sendov conjecture—posed in 1958 by Bulgarian mathematician Blagovest Sendov—states that if all zeros of a complex polynomial lie in a disk of diameter 2, then every zero has a critical point (a zero of the derivative) within distance 1. For 67 years no complete proof existed. Terence Tao's 2020 breakthrough proved an absolute degree threshold N above which the conjecture automatically holds, published in Acta Mathematica in 2022, but left finitely many low-degree cases. In 2026, mathematician Lech Mazur used a hybrid AI toolchain (reportedly combining OpenAI and Anthropic models) to generate roughly 90,000 lines of Lean 4 proof code for the remaining cases. Human collaborators, with Tao as an independent verifier, compressed the proof to about 15,000 lines (a 6:1 ratio) using geometric identities, Möbius transformations, and Maclaurin inequalities, reducing Lean 'sorry' gaps from ~4,200 to 11. The related Phelps-Rodriguez conjecture fell as a corollary, and a new proof of Rubinstein's 1994 theorem emerged as a byproduct. The episode highlights a new human–machine–Lean verification paradigm for formal mathematics.

Sendov Conjecture: A 67-Year-Old Problem Closed with AI-Generated, Human-Compressed Lean Proofs

In 1958, Bulgarian mathematician Blagovest Sendov proposed a seemingly intuitive claim: if all zeros of a complex polynomial lie within a disk of diameter 2, then every zero has a critical point (a zero of the polynomial's derivative) within distance 1. For 67 years, no one produced a complete proof. In August 2026, the conjecture was finally closed through a collaboration involving AI systems, Lean proof assistants, and human mathematicians including Fields Medalist Terence Tao.

Key Concepts

Zero: a complex number z with P(z) = 0.
Critical point: a complex number z with P'(z) = 0.
Unit disk: the disk of radius 1 centered at the origin in the complex plane.

Early literature sometimes calls it the Ilieff–Sendov conjecture due to attribution ambiguities within the Bulgarian school.

Timeline

1958 — Sendov proposes the conjecture.
1979 — Paul Erdős and Shiing-Shen Chern take interest, proposing auxiliary conjectures.
1987 — Proven for polynomials of degree n ≤ 5.
1990s — Special cases up to n ≤ 8 resolved.
2014–2020 — Terence Tao works on critical point–zero distance problems; in December 2020 he announces a proof that an absolute constant N exists such that the conjecture holds for all degrees ≥ N (published in *Acta Mathematica*, 2022). The finitely many remaining low-degree cases remained open—potentially enormous in number.
2026 — Lech Mazur closes the gap with AI-generated arguments plus Lean formalization; the Phelps-Rodriguez conjecture is resolved simultaneously.

The AI-Assisted Proof

In early 2026, Lech Mazur (affiliated with UC Berkeley and Stevens Institute of Technology) used an AI system—per his May 2026 blog, a toolchain combining OpenAI and Anthropic models—to generate a candidate proof for the remaining finite-degree cases. Rather than a single conceptual argument, the AI produced a case-enumeration search tree: for each remaining degree, it enumerated coefficient spaces and either refuted counterexamples or constructed witnesses.

The output was roughly 90,000 lines of Lean 4 code, each line machine-checked by the Lean kernel.

Compression from 90,000 to 15,000 Lines

Mazur and collaborators (with Tao as an independent verifier) reorganized the AI's exhaustive case-by-case proofs, which often restated the same algebraic structure in disguise. Humans contributed three key moves:

1. Extracting geometric identities — using polynomial barycenters, inversion at the origin, and origin constraints to merge hundreds of cases into a few single lemmas. 2. Möbius transformations — normalizing disk coordinates so that "distance ≤ 1" is preserved, turning discrete case assignments into symmetric inequalities. 3. Maclaurin inequalities — bounding polynomial coefficients continuously, eliminating the need for case-by-case enumeration.

| Stage | Lean lines | Meaning | | --- | ---: | --- | | AI draft | ~90,000 | Exhaustive case search tree | | After human restructuring | ~15,000 | Geometric identities + Möbius + Maclaurin framework | | Compression ratio | ~6:1 | Equivalent reformulation of the same proof |

The lesson: AI excels at spreading out possibilities; humans excel at folding them together.

Phelps-Rodriguez Conjecture Falls Too

The Phelps-Rodriguez conjecture relaxes Sendov's hypothesis, allowing one outlier zero. It was long considered harder. But the geometric toolkit from the Sendov proof transferred almost unchanged, and the team resolved it as a light extension—an example of surrounding open problems falling in clusters once a paradigm matures.

Tao's Independent Verification

In early August 2026, Terence Tao announced end-to-end independent verification of the Lean code:

1. Regeneration: he re-ran proof generation from the other end of the AI toolchain, confirming the output was not a one-off. 2. Lemma-by-lemma checking: he mapped key lemmas onto his 2020 analytic framework, confirming the compressed and uncompressed arguments were mathematically equivalent. 3. Error pattern analysis: Lean sorry placeholders (admitted unproven states) dropped from ~4,200 in the AI draft to 11 after compression—all "obvious but syntactically awkward" gaps.

A Three-Way Division of Labor

The paradigm is neither "human thinks, machine executes" nor "machine generates, human reviews," but three parallel actors:

Machine: enumerates possibilities, drafts lemmas and Lean code.
Human: selects meaningful subproblems, identifies shared geometric structure, introduces tools (Möbius/Maclaurin), compresses arguments, fills remaining gaps.
Lean: strict type-checking, the merciless referee.

Community Reaction and Outlook

At an August 2026 Leiden workshop on formal mathematics frontiers, participants adopted a short "Leiden Declaration": formal proofs become strong evidence for finite-case-closure claims; journals should accept Lean proof manuscripts; and AI-generated argument nodes must be transparently disclosed. Meta-auditing of AI-generated Lean code is emerging as a new research activity—one unpublished estimate suggests auditing at Sendov's scale requires 2–3 full-time mathematicians for 4 months.

On extrapolation: the Sendov paradigm does not automatically extend to related problems. Borcea's and Schmeisser's conjectures may partially reuse it, but Smale's 18th problem (the high-dimensional analogue) cannot—Möbius transformations have no high-dimensional counterpart. That is mathematical honesty, not failure.

Byproduct: Rubinstein's 1994 theorem on critical point–zero distances for intermediate degrees received a new, more elementary proof via Maclaurin inequalities.

Takeaways:

1. Formal proofs are becoming infrastructure, not luxury—claims of closing major open problems without Lean code will face skepticism. 2. AI-assisted proof is accepted as a tool: unnamed, but equally scrutinized. 3. The "compression ratio" (AI draft → human rewrite) may become a proxy metric for genuine understanding. Mazur's 6:1 will be cited for years. 4. This was not AI beating mathematicians—it was AI saving mathematicians from typing. The key insight (Möbius + Maclaurin) came from human perspective, not the machine.

> Sendov was 30 when he asked an "obvious" question over a sketch. Today an AI wrote the clumsiest part of the answer. But the 67 years of weight behind the word "obvious" is not something AI can—or should—carry.

---

*Written late August 2026, on the day the Lean-formalized proof of the Sendov conjecture was accepted by the Annals of Mathematics.*