Proposed
Original AI-assisted proof announcement ↗
Mazur’s all-degree proof and initial formalization.
Sendov conjecture: original proof · Original proof dated 5 August 2026 →
Observed Oct 13, 2026
Theorem · version 1
A critical point within distance one
Earlier version 1. View current version 2 →
Statement
For every p ∈ ℂ[X] of degree n ≥ 2 whose zeros all satisfy |z| ≤ 1, and every a with p(a) = 0, there is ζ ∈ ℂ with p′(ζ) = 0 and |ζ − a| ≤ 1.
Assumptions
- Degree at least two.
- Every polynomial zero lies in the closed unit disk.
Scope
Full Sendov statement, including repeated roots and boundary roots.
Evidence
Source reports
These reports have different dispositions. Differences in date, scope or assessment stage do not by themselves establish a mathematical dispute.
Proved
Sendov and the sharper form proved in the exposition ↗
All degrees n ≥ 2 with the stated disk assumption.
Observed Oct 13, 2026
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 v1 · 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 · 3
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 →
Proposed
Original AI-assisted proof announcement ↗
Mazur’s all-degree proof and initial formalization.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-sendov-distance-one
- Statement version
- 1
- SHA-256
- e17fc047aa70cfb74d93c63d5911a70baa8775d689c78866775803b673ced3e7