Problem detail · source-aware
VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
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.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement fidelity, correctness, priority, or novelty.
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.
Provider: OpenAI · Prompt public: unknown · Independence: unknown
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.
Correctness: supported · statement fidelity: audited · peer review: none
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.
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.