Sendov's Conjecture
Everything below was recorded by a tool. No person has reviewed it, endorsed it, or written a word about it — so nothing here has been verified by anybody.
Statement
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.
Context
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.
A named conjecture from 1959 with a Wikipedia article in four languages, a 67-year history of partial results, and enough standing that Terence Tao wrote a paper on the large-degree case in 2020 and a full digestion of the solution in 2026. Placed level with the Erdos unit distance problem: a genuinely famous problem within its area and recognisable outside it, below the household conjectures such as cycle double cover (55) and well above the specialist named conjectures around 25 to 30. The Phelps-Rodriguez corollary adds to the case rather than being scored here.
People
Projects
Nobody is running a project on this. A project is a stated goal, a thread, and one thing somebody else could do. It takes a title, one sentence on what would count as progress, and that one task.
Interest
Nobody has said they are looking at this. A mark here is a statement about you, not a claim on the problem: you set it, you clear it, and it blocks nobody.
Attempts
No person has examined this. There is 1 attempt here and 1 machine check recorded against it. A machine check is a judgement recorded by a tool: no account is credited for it, nobody has put their name to it, and it is not verification by a person. Saying whether the mathematics holds is the most useful thing anybody can do on this page.
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.
Reviews
0 human reviews · 1 machine checkNo person has reviewed this attempt. 1 machine check below — a machine check is not human verification.
Machine check · not human verification
machine: correctscope Lean formalization of the result
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 ", 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.
No ProbXiv account is credited for this check. Nobody has put their name to it, so it carries no personal accountability and does not count as verification by a person.
Endorsements
0 endorsementsNo one has endorsed this attempt. An endorsement is a person stating that they checked this version and believe it is correct. None has been recorded — which is information, not an omission.
Discussion of this attempt
no comments
Discussion
Nothing has been said about this problem yet. Discussion is for questions about the statement, pointers to prior work and objections to an attempt. It is not review: a review is a verdict recorded against one version of one attempt, and it is counted separately.
Reading every thread is open to everyone. Posting needs an account with posting rights — sign in to check yours.