openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

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
Frontier 1 report →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Earlier version 1 of this page. View current →

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.

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

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.

A boundary example with distance exactly oneA unit circle contains the three cube roots of one on its boundary. The distinguished root a = 1 is connected to the centre ζ = 0 by a segment of length one.p(z) = z³ − 1a = 1ζ = 0distance 1All three roots: |z| = 1
Understand the equality exception● Proved under stated assumptionsRead the full distance-one statementQuestion scope

Select a statement below for its scope and evidence. The text view describes the complete drawing.

Text version

A unit circle contains the three cube roots of one on its boundary. The distinguished root a = 1 is connected to the centre ζ = 0 by a segment of length one.

Coordinates in the drawing are illustrative unless the caption specifies an exact example.

  1. Understand the equality exception

    Proved

    Strict distance and the equality exception

    The stronger Phelps–Rodriguez conclusion includes its precise exceptional family; it is not a second formulation of the same distance bound.

    Strict distance and the equality exception →

  2. Read the full distance-one statement

    Proved

    A critical point within distance one

    Full Sendov statement, including repeated roots and boundary roots.

    A critical point within distance one →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

Variants and analogues 1

Background 1

Connections

Consequences 1

Assuming Strict distance and the equality exceptionProved

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

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. 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.

  2. 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.

  3. 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.

    Also on the Frontier: Sendov and Phelps–Rodriguez conjectures

  4. 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.

  5. 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.

Full history with sources →

Evidence

Literature

1 preprint · 2 projects

Status OpenMath assessment · Oct 13, 2026.

Formal

2 complete proofs

2 formalizations below ↓

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

Open formal source ↗

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.sendov

Commit 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d

Strict distance and the equality exception →

Lean: the sharp Phelps–Rodriguez formComplete formal proof reported externally

Open formal source ↗

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_rodriguez

Commit 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

Bibliography 3

Research activity · 1 entry

Contributions

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.

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 →

Sendov and Phelps–Rodriguez in Lean · sources & artifacts →

Selected literature; source observations and coverage limits are retained in the publication details.

Record details
Record version
1
Classification
MSC2020 30C15
Prerequisite level
graduate
Source observations & version history →