Sendov's Conjecture

Let $p$ be a complex polynomial of degree $n \ge 2$ whose zeros all lie in the closed unit disk. Then for every zero $a$ of $p$ , there exists a critical point $\zeta$ of $p$ such that $|\zeta-a| \le 1$ .

This is the standard Sendov statement and exactly matches the theorem Mazur formalized.

Result: Proved(see note)
Status: Resolved
AI contribution: AI-discovered
Method: Argument
Field: Complex analysis
Posed by: Blagovest Sendov
Year posed: 1959
Years open: 67y
Solved: 2026-08-05
Model: GPT-5.6 Pro
Vendor: OpenAI
Collaborators: Lech Mazur
Verification: Lean-verified
Publication: Preprint
Significance: 40 / 100
Disclosed cost: —
Wikipedia: 4 languages

What was actually shown

Sendov's conjecture is resolved for every degree n >= 2, closing a gap that had stood since 1959: degrees up to eight were settled piecemeal between 1969 and 1999, and Tao's 2020 result covered all sufficiently large degrees without ever specifying the threshold, leaving the middle range open. Tao's digestion establishes the stronger interior form of the statement, which resolves the Phelps-Rodriguez conjecture in full generality as a consequence - a second conjecture falling out of the same argument, and one that likely merits its own entry. Two independent Lean developments now exist: Mazur's original at roughly 90,000 lines and Tao's streamlined version at about 15,000.

What the AI did

GPT-5.6 Pro contributed substantially to the discovery and derivation of the proof, including mathematical exploration, proof development, exact computational testing, and adversarial auditing. Lech Mazur directed the research workflow, selected and reconciled model outputs, and authored the resulting manuscript. A separate Lean 4 development proves the exact statement of Sendov's conjecture.

Verification

Independently verified twice over, and this site audited the formal artifact itself on 13 August 2026. The decisive external check is Terence Tao's post of 12 August 2026, "A digestion of the proof of Sendov's conjecture": he writes that "Lech Mazur was able to use an AI tool to resolve Sendov's conjecture for all $n \ge 2$ ", reports formalizing the whole argument in Lean himself at about 15,000 lines against the original's roughly 90,000, and concludes that it resolves both the Sendov and Phelps-Rodriguez conjectures in full generality. Tao proved the large-degree case in 2020, so this is expert verification by the person best placed to give it, and it carries the tier. Separately, this site audited Mazur's Lean package. SendovConjecture in Sendov/Statement.lean is exactly the conjecture, correctly quantified and shadowed nowhere. Across all 1,160 first-party files there are zero sorry, zero admit, zero custom axiom declarations and - the one that matters for an autonomous prover - zero native_decide; the 1,117 decide calls are kernel-checked, and the axiom profile is exactly propext, Classical.choice and Quot.sound. All 1,160 file hashes match the published evidence record byte for byte. What could not be checked is the build: the bundle ships no lakefile or manifest and excludes Mathlib, so it cannot be recompiled as distributed, a gap ProofAtlas's own evidence file is candid about. This entry rests not on that internal status but on Tao's independent digestion.

Sources

Related entries

Same work resolves bothPhelps–Rodriguez Conj.

Submitted by HiddenHawk615 on 13 Aug 2026