A critical point within distance one →
- Distance
- At most one, for every root
- Exceptions
- None under the stated polynomial hypotheses
Complex analysis · Conjecture
Sendov’s conjecture
If every zero of a complex polynomial lies in the closed unit disk, must each zero be within distance one of a zero of its derivative?
ProvedOpenMath assessment · Oct 13, 2026
- Literature: 1 published paper · 1 preprint · 2 projects
- Formal: 2 complete proofs
- Computation: None recorded
- Review: Not yet reviewed
Frontier 1 report →
Overview
Known
The cited exposition proves Sendov for every degree n ≥ 2 and gives the sharper Phelps–Rodriguez theorem. Public Lean endpoints cover both conclusions.
Latest
Precise statement
A nonzero complex polynomial of degree n ≥ 2, with every root a satisfying |a| ≤ 1. A critical point is a zero of p′, not another zero of p. Roots may repeat.
Definitions
- Critical point
- A zero of the polynomial’s derivative. Sendov asks for one within distance one of each zero of the original polynomial.
Background
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
Visual setup
Closing the gap in degree
Low degrees were settled by 1999 and all large degrees by Tao’s 2020 paper, but n₀ was not explicit, so the degrees in between stayed open until the 2026 proof covered every n.
Reading boundary. The middle column is not a fixed range: Tao’s n₀ is not explicit, so before 2026 no finite computation was known to close the gap.
Degree n
Brown–Xiang 1999
Degree n 2–8: Holds there.Proved● Proved under stated assumptions
Tao 2020
Degree n ≥ n₀: Holds there.Proved● Proved under stated assumptions
2026 proof
Degree n 2–8–≥ n₀: Holds there.Every degree● Proved under stated assumptions
✓ Holds thereEach cell links to its statement and status
Explore
Move the zeros yourself
Drag the zeros of a polynomial anywhere in the unit disk. The crosses are the zeros of its derivative; the dashed circle of radius one around the selected zero always reaches one of them.
Reading boundary. An illustration for the polynomial on screen only: it computes, it does not prove, and numerical roots can be inaccurate near repeated zeros. The theorem is the linked statement.
● zeros of p (drag them)× critical points: zeros of p′dashed: radius one around the selected zero
Degree 5. Selected zero a = 0.800 + 0.300i. Nearest critical point at distance 0.251 — within one, as the theorem says.
Visual setup
A boundary example with distance exactly one
For p(z) = z³ − 1, all three roots lie on the unit circle. The derivative has its only zero at the centre, with multiplicity two.
Reading boundary. This exact example illustrates the equality exception. It does not prove the theorem for arbitrary polynomials.
Equality only for c(zⁿ − aⁿ) (Phelps–Rodriguez)● Proved under stated assumptionsSendov’s distance-one statementQuestion scope
All three roots lie on the unit circle; the derivative 3z² vanishes only at the centre.
Results
The question 1
- ProvedA critical point within distance oneMazur 2026 · per Tao 2026Formalized
Full Sendov statement, including repeated roots and boundary roots.
Theorem · Primary formulation
ProvedMazur 2026 · per Tao 2026A critical point within distance one
For every of degree n ≥ 2 whose zeros all satisfy |z| ≤ 1, and every a with p(a) = 0, there is ζ ∈ ℂ with p′(ζ) = 0 and .Assumptions
- Degree at least two.
- Every polynomial zero lies in the closed unit disk.
- Distance
- At most one, for every root
- Exceptions
- None under the stated polynomial hypotheses
In this problem
Full Sendov statement, including repeated roots and boundary roots.
Formal proofs
- Lean: Sendov for every degree ↗Complete formal proof reported externally
Sources
Special cases 2
- ProvedSendov for degree at most eightBrown & Xiang 1999 · per Tao 2022
The low-degree cases, settled before the general proof.
Theorem · Special case
ProvedBrown & Xiang 1999 · per Tao 2022Sendov for degree at most eight
For every polynomial p of degree n with 2 ≤ n ≤ 8 whose zeros all satisfy |z| ≤ 1, each zero a has a critical point ζ with |ζ − a| ≤ 1.Assumptions
- Complex polynomials of degree 2 to 8 with all zeros in the closed unit disk.
In this problem
A range of degrees proved before the full statement.
The low-degree cases, settled before the general proof.
Sources
- ProvedSendov for all sufficiently large degreeTao 2022
Large degree only; the degrees between 9 and n₀ were left open until the 2026 proof.
Theorem · Special case
ProvedTao 2022Sendov for all sufficiently large degree
There is a constant n₀ such that for every polynomial p of degree n ≥ n₀ whose zeros all satisfy |z| ≤ 1, each zero a has a critical point ζ with |ζ − a| ≤ 1.Assumptions
- Complex polynomials of degree at least n₀ with all zeros in the closed unit disk.
- n₀ is not explicit.
In this problem
A range of degrees proved before the full statement.
Large degree only; the degrees between 9 and n₀ were left open until the 2026 proof.
Sources
Variants and analogues 1
- ProvedStrict distance and the equality exceptionMazur 2026 · per Tao 2026Formalized
The stronger Phelps–Rodriguez conclusion includes its precise exceptional family; it is not a second formulation of the same distance bound.
Theorem · Different statement · related variant
ProvedMazur 2026 · per Tao 2026Strict distance and the equality exception
Under Sendov’s assumptions, every zero a has a critical point ζ with , unless |a| = 1 and for a nonzero complex constant c.Assumptions
- Degree n ≥ 2.
- All zeros of p are in the closed unit disk.
- Distance
- Strictly less than one
- Exceptions
- A boundary root |a| = 1 with p(z) = c(zⁿ − aⁿ), c ≠ 0
In this problem
The stronger Phelps–Rodriguez conclusion includes its precise exceptional family; it is not a second formulation of the same distance bound.
Formal proofs
- Lean: the sharp Phelps–Rodriguez form ↗Complete formal proof reported externally
Sources
Background 1
- ProvedWhy the radius one is sharpTao 2026
The boundary example prevents a uniform strict radius-one conclusion without exceptions.
Theorem · Supporting result
ProvedTao 2026Why the radius one is sharp
For , the root a = 1 has distance exactly one from the only critical point ζ = 0, since .Assumptions
- This is the exact cubic example p(z) = z³ − 1.
- Distance
- Exactly one from a = 1 to ζ = 0
- Polynomial
- p(z) = z³ − 1; p′(z) = 3z²
In this problem
The boundary example prevents a uniform strict radius-one conclusion without exceptions.
Sources
Compare statements · 3
Each row is a separate assertion. Its assumptions determine which question it answers.
Strict distance and the equality exception →
- Distance
- Strictly less than one
- Exceptions
- A boundary root |a| = 1 with p(z) = c(zⁿ − aⁿ), c ≠ 0
Why the radius one is sharp →
- Distance
- Exactly one from a = 1 to ζ = 0
- Polynomial
- p(z) = z³ − 1; p′(z) = 3z²
Connections
Consequences 1
Assuming Strict distance and the equality exceptionProved
The theorem also identifies when equality is unavoidable
Under stated assumptionsThe stronger conclusion explains why the boundary family must be excluded from a strict distance bound; the cubic example makes that limitation visible.
Limit No universal radius smaller than one follows.
Sources & review
Supporting statements
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
Source-grounded explanation · independent explanation review: pending.
Approaches
How the problem is attacked, and what each line of attack cannot yet reach.
Roots and critical points are linked by identities
The argument uses polynomial identities, inequalities and exact rational certificates after treating the centre and boundary separately.
Cannot yet reach A plotted collection of roots cannot replace the all-degree argument.
Sources & review
Supporting statements
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
Source-grounded explanation · independent explanation review: pending.
Timeline
A second, streamlined Lean formalizationFormalization
The pinned teorth/sendov development exposes both full theorem endpoints.
This is source-reported proof checking, not an OpenMath execution.
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
A human-readable proof and sharper conclusionAssessment
Terence Tao’s mathematical digestion also yields the Phelps–Rodriguez equality classification.
The argument descends from Mazur’s proof; exposition does not establish a new independent discovery.
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
Mazur’s AI-assisted all-degree proofProposal
Lech Mazur directed the original discovery and initial formalization with GPT-5.6 Pro.
The original artifact and the later streamlined formalization are separate evidence.
- Sendov conjecture: original proof ↗Original proof dated 5 August 2026
Boundary case and equality classificationFoundation
Rubinstein’s boundary-root theorem supplies the exceptional polynomial family.
This historical result is credited in the exposition and is not attributed to the 2026 AI workflow.
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
Earlier partial resultsFoundation
The cited exposition records all degrees through eight and all sufficiently large degrees as already established.
These results left an intermediate-degree gap; no exact degree threshold is supplied here.
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
Evidence
| Literature | 1 published paper · 1 preprint · 2 projects Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | Reported in sources: The full Sendov and Phelps–Rodriguez statements have pinned public Lean sources. Completion is reported by the project; OpenMath has not executed their builds. |
| Computation | None recorded |
| Review | Not yet reviewed OpenMath assessment: The cited exposition proves Sendov for every degree n ≥ 2 and gives the sharper Phelps–Rodriguez theorem. Public Lean endpoints cover both conclusions. Source comparison and page curation only; independent mathematical review is pending. OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027 Collection last checked Oct 13, 2026. |
Formalizations
A critical point within distance one →
Lean: Sendov for every degreeComplete formal proof reported externally
Complete formal proof reported externally
Source-reported complete. The separate Challenge file contains deliberate statement placeholders; the project reports no holes in the proof endpoint.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Sendov.sendovCommit 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d
Strict distance and the equality exception →
Lean: the sharp Phelps–Rodriguez formComplete formal proof reported externally
Complete formal proof reported externally
Source-reported complete, including the equality classification. Independent OpenMath execution and review remain pending.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Sendov.phelps_rodriguezCommit 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Sources
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Start here
- Introduction
A digestion of the proof of Sendov’s conjecture →Read the setting and notation before comparing the results.
- Proof source
Sendov conjecture: original proof →Read the mathematical argument; inspect its statement for assessment and scope.
- Formal source
Sendov and Phelps–Rodriguez in Lean →Inspect the formal statement, assumptions and reported checks.
Bibliography 4
- Sendov conjecture: original proof →
Lech Mazur · Preprint · Aug 5, 2026
Original proof dated 5 August 2026
- A digestion of the proof of Sendov’s conjecture →
Terence Tao · Project documentation · Aug 12, 2026
Conjectures 1–3 and proof, with provenance remarks
- Sendov and Phelps–Rodriguez in Lean →
Terence Tao · teorth/sendov project · Project documentation · Aug 19, 2026
README provenance and trust; Sendov/Conjecture.lean
- Sendov’s conjecture for sufficiently high degree polynomials →
Terence Tao · Published · 2022
Research activity · 1 entry
Formalization
Discovery, exposition and formalization
Mazur and GPT-5.6 Pro supplied the original result; Tao digested its mathematics and directed the second formalization, whose project credits Claude Opus 5.
Two formalizations of a descended argument do not automatically constitute two independent mathematical proofs.
Related statements · context, not additional proved progress
Sendov conjecture: original proof · sources & artifacts →
A digestion of the proof of Sendov’s conjecture · sources & artifacts →
Selected literature; source observations and coverage limits are retained in the publication details.
Contributors
Original direction and discovery: Lech Mazur with GPT-5.6 Pro. Mathematical digestion: Terence Tao with AI assistance. Second Lean development: Tao directing Claude Opus 5.
Authors & roles
Sendov conjecture: original proof →
Lech Mazur
Lech Mazur directed GPT-5.6 Pro discovery and formal work; mathematical direction, model work and later exposition are distinct contributions.
A digestion of the proof of Sendov’s conjecture →
Terence Tao
Terence Tao performed mathematical digestion and simplification with substantial AI assistance; this descends from Mazur’s argument and is not an independent discovery route.
Sendov and Phelps–Rodriguez in Lean →
Terence Tao · teorth/sendov project
The project reports Claude Opus 5 wrote essentially all Lean source under the author’s direction and review; this is a second formalization of the same mathematical argument.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.
Record details
- Record version
- 8
- Classification
- MSC2020 30C15
- Prerequisite level
- graduate