A streamlined exposition of Mazur’s argument gives Sendov and the sharper Phelps–Rodriguez conclusion, with its boundary equality cases.
Public manuscript or exposition; publication does not imply independent OpenMath review.
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
A streamlined exposition of Mazur’s argument gives Sendov and the sharper Phelps–Rodriguez conclusion, with its boundary equality cases.
Passage ID: sendov-conjecture:entry:digestion:v1
Source item: digestion
Source record: sendov-conjecture:source:digestion:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v8
Source assessment
Proved
Sendov and the sharper form proved in the exposition
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026
Formal declaration
Lean: the sharp Phelps–Rodriguez form
Scope
Strict distance and the equality exception
Source assessment
Proved
Sendov and the sharper form proved in the exposition
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026
Source assessment
Proved
Sendov and the sharper form proved in the exposition
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026
Formal declaration
Lean: Sendov for every degree
Scope
A critical point within distance one
Research activity
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.
History
A human-readable proof and sharper conclusion
History
Boundary case and equality classification
Further reading
Read the setting and notation before comparing the results.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
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
Sendov.phelps_rodriguezCommit 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d
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
Sendov.sendovCommit 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d
Recorded authorship
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.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
A digestion of the proof of Sendov’s conjecture
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗