The pinned public source states full Sendov and Phelps–Rodriguez endpoints and reports only the standard Lean logical axioms for their proofs.
Public formal source; build and independent mathematical review are separate checks.
1 cited passage ↓1 problem ↓Record 1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The pinned public source states full Sendov and Phelps–Rodriguez endpoints and reports only the standard Lean logical axioms for their proofs.
Passage ID: sendov-conjecture:entry:lean:v1
Source item: lean
Source record: sendov-conjecture:source:lean: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
Full Lean endpoints reported complete
Sendov.sendov and Sendov.phelps_rodriguez.
Observed Oct 13, 2026
Formal declaration
Lean: Sendov for every degree
Scope
A critical point within distance one
Source assessment
Proved
Full Lean endpoints reported complete
Sendov.sendov and Sendov.phelps_rodriguez.
Observed Oct 13, 2026
Formal declaration
Lean: the sharp Phelps–Rodriguez form
Scope
Strict distance and the equality exception
Source assessment
Proved
Full Lean endpoints reported complete
Sendov.sendov and Sendov.phelps_rodriguez.
Observed Oct 13, 2026
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 second, streamlined Lean formalization
History
Boundary case and equality classification
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Resource revision: 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
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
Recorded authorship
Terence Tao · teorth/sendov project
Terence Tao, teorth/sendov project
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.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Sendov and Phelps–Rodriguez in Lean
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗