Sendov's conjecture proved for every degree
For every complex polynomial of degree at least two whose zeros all lie in the closed unit disk, each zero has a critical point of the polynomial within distance one, closing a question open since 1959.
- Lab
- Independent
- Model
- GPT-5.6 Pro
- Field
- Mathematics
- Date
- 2026-08-05
- Human collaborators
- Lech Mazur
- Problem posed
- 1959 · open 67 yrs
Sources
Original work
Independent commentary
What was found
Sendov's conjecture states that if every zero of a complex polynomial of degree n at least two lies in the closed unit disk, then every zero has a critical point within distance one. Degrees up to eight were settled piecemeal between 1969 and 1999, and Tao proved the conjecture for all sufficiently large degree in 2020 without specifying the threshold, which left the middle range open. Lech Mazur, working with GPT-5.6 Pro, produced an argument covering every degree along with a Lean development of roughly 90,000 lines. Terence Tao then digested the proof, describing it as remarkably elementary with no complex analysis used beyond the fundamental theorem of algebra, and formalized the entire argument himself in about 15,000 lines. He reports that the same argument resolves the Phelps–Rodriguez conjecture in full generality.
Novelty check
Sendov's conjecture is a named 1959 problem with its own Wikipedia article in four languages and a partial-results literature spanning 67 years. Tao's 2020 paper on the sufficiently-high-degree case (arXiv:2012.04125) states the general case as open, which fixes the prior state of the art precisely. No earlier proof covering all degrees appears in the literature, and the Phelps–Rodriguez corollary is new with it. The result is a new proof, not a retrieval. On priority between the two formalizations: Palomar's record for Tao's development notes that it shares no code with Mazur's, was written from the blog-post digestion rather than from that proof, and that priority for the first machine-checked proof of Sendov's conjecture belongs to Mazur's ProofAtlas work.
Caveats and known objections
Not peer-reviewed. Mazur's own Lean package cannot be recompiled as distributed: the published bundle ships no lakefile or manifest and excludes Mathlib, so the formal grade rests on Tao's independent formalization rather than on the original artifact. Autonomy graded collaborative rather than ai-led: the disclosure credits GPT-5.6 Pro with substantial contribution to the discovery and derivation of the proof, including exploration, proof development, exact computational testing and adversarial auditing, but it also has Mazur directing the research workflow and selecting and reconciling the model's outputs, which is mathematical judgment rather than cleanup. The weaker defensible reading applies.
Independent checks
Terence Tao: digested the argument and formalized the whole of it in Lean independently, at about 15,000 lines against the original's roughly 90,000, and states that it resolves both the Sendov and Phelps–Rodriguez conjectures in full generality · link ↗
Machine-checked elsewhere
PalomarPALOMAR-2026-08-13-000001
teorth/sendov at e356ef6d706c · checked 2026-08-13
ProvedSendovConjecture.sendovSendovConjecture.phelps_rodriguez
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Permitted axioms are exactly propext, Quot.sound and Classical.choice, so the development adds none of its own. This is the artifact the formal grade already rested on, now checked by someone other than its author.
sendov-conjecture
That a recorded Lean build passed with no unfinished proof steps, under its own evidence contract, which a record can satisfy for checking while still failing for acceptance.
ProofAtlas records that the build passed with no unfinished proof steps, and that the record has not reached its accepted-result status, which needs four independent reviews. Its recorded build is not the same claim as the published bundle being rebuildable; this entry's caveat that the distributed package ships no lakefile or manifest still stands.
The open problem
315904
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
Also recorded at
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Disagree with these grades?
Bring a citation: a grade moves on evidence, not on argument.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
History of this entry
- CorrectedRecorded the ProofAtlas record for Mazur's formalization as a registration. It was previously carried as a research source, which a registry listing is not. The paper it accompanies stays a source, and no grade moved. source ↗
- CorrectedRecorded priority for the first machine-checked proof, which belongs to Mazur's ProofAtlas formalization rather than to Tao's independent one. Neither grade moved.
- CorrectedRecorded the vibemathed and MathDB records for this result as registrations. The vibemathed link it replaces was classified as commentary, which a registry listing is not.
- CheckedPalomar registered Tao's Lean development as PALOMAR-2026-08-13-000001, mechanically confirming that it typechecks against both stated theorems at a pinned commit under the three standard axioms. source ↗
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Sendov's conjecture proved for every degree. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-08-05-sendov-conjectureBibTeX
@misc{whataifound-independent-2026-conjecture,
title = {Sendov's conjecture proved for every degree},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-08-05-sendov-conjecture}
}