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
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.
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 ↗
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.
Entry history (1 event)
- 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}
}