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 1
Why the radius one is sharp
Earlier version 1. View current version 2 →
Statement
For p(z) = z³ − 1, the root a = 1 has distance exactly one from the only critical point ζ = 0, since p′(z) = 3z².
Assumptions
- This is the exact cubic example p(z) = z³ − 1.
Scope
The boundary example prevents a uniform strict radius-one conclusion without exceptions.
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
Connections
In this problem · publication v1 · Selected context
Sendov’s conjecture →
Supporting result · 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-sharp-radius-example
- Statement version
- 1
- SHA-256
- 93f517daaab3d815166def6efd92d624d4610723c66ca2b79d7a5a332981cf0e