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
A critical point within distance one
Statement
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.
Scope
Full Sendov statement, including repeated roots and boundary roots.
- Distance
- At most one, for every root
- Exceptions
- None under the stated polynomial hypotheses
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: Sendov for every degree ↗
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
Connections
In this problem · publication v8 · Selected context
Sendov’s conjecture →
Primary formulation · 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.
Sendov conjecture: original proof →
- Original proof dated 5 August 2026 → · Original passage ↗
Recorded wording
A directed AI workflow reports a proof of Sendov for every degree at least two; the original proof and formalization preceded Tao’s exposition.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
Lech Mazur · Preprint · Publication date Aug 5, 2026
Public manuscript or exposition; publication does not imply independent OpenMath review.
Revision & attribution
Source revision: 2026-08-05. Observed Oct 13, 2026.
Lech Mazur directed GPT-5.6 Pro discovery and formal work; mathematical direction, model work and later exposition are distinct contributions.
Source updated Aug 5, 2026.
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-distance-one
- Statement version
- 2
- SHA-256
- 232019282dacaf406a60b1ee1d9ebf0d2468ffcc1eb96966bc7c9a6b0093b646