Proved
Sendov and the sharper form proved in the exposition ↗
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026
Theorem · version 2
Strict distance and the equality exception
Statement
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.
Scope
The stronger Phelps–Rodriguez conclusion includes its precise exceptional family; it is not a second formulation of the same distance bound.
- Distance
- Strictly less than one
- Exceptions
- A boundary root |a| = 1 with p(z) = c(zⁿ − aⁿ), c ≠ 0
Evidence
Source reports
Proved
Full Lean endpoints reported complete ↗
Sendov.sendov and Sendov.phelps_rodriguez.
Sendov and Phelps–Rodriguez in Lean · README provenance and trust; Sendov/Conjecture.lean →
Observed Oct 13, 2026
Formal proofs
Lean: the sharp Phelps–Rodriguez form ↗
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
Connections
In this problem · publication v2 · Selected context
Sendov’s conjecture →
Different statement · related variant · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v8
Sendov’s conjecture →
Different statement · related variant · Proved
Relationship not independently reviewed. This concerns its use in this problem.
Sources
A digestion of the proof of Sendov’s conjecture →
- Conjectures 1–3 and proof, with provenance remarks → · Original passage ↗
Recorded wording
A streamlined exposition of Mazur’s argument gives Sendov and the sharper Phelps–Rodriguez conclusion, with its boundary equality cases.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Terence Tao · Project documentation · Publication date Aug 12, 2026
Public manuscript or exposition; publication does not imply independent OpenMath review.
Revision & attribution
Source revision: 2026-08-12. Observed Oct 13, 2026.
Terence Tao performed mathematical digestion and simplification with substantial AI assistance; this descends from Mazur’s argument and is not an independent discovery route.
Source updated Aug 12, 2026.
Sendov and Phelps–Rodriguez in Lean →
- README provenance and trust; Sendov/Conjecture.lean → · Original passage ↗
Recorded wording
The pinned public source states full Sendov and Phelps–Rodriguez endpoints and reports only the standard Lean logical axioms for their proofs.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Terence Tao · teorth/sendov project · Project documentation · Publication date Aug 19, 2026
Public formal source; build and independent mathematical review are separate checks.
Sendov and Phelps–Rodriguez in Lean — pinned source ↗No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Revision & attribution
Source revision: 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d. Observed Oct 13, 2026.
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.
Source updated Aug 19, 2026.
Sendov and Phelps–Rodriguez in Lean — pinned source: 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 2
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Full Lean endpoints reported complete ↗
Sendov.sendov and Sendov.phelps_rodriguez.
Observed Oct 13, 2026 · Source passage →
Proved
Sendov and the sharper form proved in the exposition ↗
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-sendov-phelps-rodriguez
- Statement version
- 2
- SHA-256
- c54a1c916ffc6f43f1f15e8f68d181b259407d69f264c03f9945d95477e945ea