Sendov's Conjecture
Let be a complex polynomial of degree whose zeros all lie in the closed unit disk. Then for every zero of , there exists a critical point of such that . 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 >= 2", reports formalizing the entire argument in Lean himself at about 15,000 lines against the original's roughly 90,000, and concludes that the argument "resolves both the Sendov conjecture and the Phelps-Rodriguez conjecture in full generality". Tao proved the sufficiently-large-degree case in 2020, so this is expert verification by the person best placed to give it, and it is what carries the tier here. Separately, this site downloaded and audited Mazur's Lean package. The definition SendovConjecture in Sendov/Statement.lean is exactly the conjecture, correctly quantified over every nonzero complex polynomial of degree at least two and every zero, declared once and shadowed nowhere. Across all 1,160 first-party Lean files there are zero sorry, zero admit and zero custom axiom declarations, and - the one that matters for an autonomous prover - zero uses of native_decide; the 1,117 decide calls are kernel-checked. The recorded axiom profile is exactly propext, Classical.choice and Quot.sound. All 1,160 file hashes in the published evidence record match the downloaded bundle byte for byte, as does Theorem.lean against its pinned artifact hash. What this site could not check is the build itself: the published bundle ships no lakefile and no lake-manifest, and excludes Mathlib, so it cannot be recompiled as distributed. ProofAtlas's own evidence file is candid about the same gap, recording buildTranscriptRecorded false, collectionProvenanceRecorded false and a publication review status of accountable_review_not_recorded. That internal status is not what this entry rests on; Tao's independent digestion and independent formalization are.
Sources
- PaperTao, Sendov's conjecture for sufficiently high degree polynomials (2020)
- Lean proofProofAtlas formalization page: exact theorem, evidence and build record
- CodeMazur's Lean package, checked source bundle (1,160 files, ~93k lines)
- Independent workTerence Tao, A digestion of the proof of Sendov's conjecture (12 Aug 2026)
- WikipediaWikipedia: Sendov's conjecture
- OtherA Computer-Assisted Proof of Sendov's Conjecture
Submitted by HiddenHawk615 on