Selected research history · publication v5

Sendov’s conjecture

Follow the ideas, results and limitations over time. This is a selected history, not a complete literature survey or a measure of how close the problem is to being solved.

Current state & remaining question →

Viewing the timeline from pinned publication v5.

5 selected milestones · Source coverage checked 2026-10-13 · Historical annotation and mathematical review remain separate.

1968 publication
Foundation
Boundary case and equality classification
Rubinstein’s boundary-root theorem supplies the exceptional polynomial family.
Scope & review: This historical result is credited in the exposition and is not attributed to the 2026 AI workflow.
Statements & sources
- Strict distance and the equality exception →
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
Historical annotation review: pending. The date refers to the publication, with the precision supported by the source.
Aug 5, 2026 announcement
Proposal
Mazur’s AI-assisted all-degree proof
Lech Mazur directed the original discovery and initial formalization with GPT-5.6 Pro.
Scope & review: The original artifact and the later streamlined formalization are separate evidence.
Statements & sources
- A critical point within distance one →
- Sendov conjecture: original proof ↗Original proof dated 5 August 2026
Historical annotation review: pending. The date refers to the announcement, with the precision supported by the source.
Aug 12, 2026 publication
Assessment
A human-readable proof and sharper conclusion
Terence Tao’s mathematical digestion also yields the Phelps–Rodriguez equality classification.
Scope & review: The argument descends from Mazur’s proof; exposition does not establish a new independent discovery.
Statements & sources
- A critical point within distance one →
- Strict distance and the equality exception →
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
Historical annotation review: pending. The date refers to the publication, with the precision supported by the source.
Aug 19, 2026 formalization
Formalization
A second, streamlined Lean formalization
The pinned teorth/sendov development exposes both full theorem endpoints.
Scope & review: This is source-reported proof checking, not an OpenMath execution.
Statements & sources
- A critical point within distance one →
- Strict distance and the equality exception →
- Sendov and Phelps–Rodriguez in Lean ↗README provenance and trust; Sendov/Conjecture.lean
Historical annotation review: pending. The date refers to the formalization, with the precision supported by the source.
Date unavailable publication
Foundation
Earlier partial results
The cited exposition records all degrees through eight and all sufficiently large degrees as already established.
Scope & review: These results left an intermediate-degree gap; no exact degree threshold is supplied here.
Statements & sources
- A critical point within distance one →
- A digestion of the proof of Sendov’s conjecture ↗Conjectures 1–3 and proof, with provenance remarks
Historical annotation review: pending. The date refers to the publication, with the precision supported by the source.

← Back to the Problem

Boundary case and equality classification

Mazur’s AI-assisted all-degree proof

A human-readable proof and sharper conclusion

A second, streamlined Lean formalization

Earlier partial results