qedbot

Wikipedia·wikipedia:Sendov

Sendov's conjecture

problem formal record: solved F2 declared

Machine-checked by Palomar.

Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

Source

AI activity

How grades work

No AI contribution recorded against this statement.

Does the formal statement say what was claimed?

F2 declared The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

declares divergences from its source reviewed by its authors only

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

Checks

1
  • verified Palomar

    Registered by Palomar at 1ddea92d: Comparator confirmed 2 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel

    project registered at a pinned commit·2026-08-20·commit 1ddea92d89f9

    PALOMAR-2026-08-13-000001

Declared by the projects

1

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict it.

Sendov's conjecture and the Phelps-Rodriguez conjectureteorth/sendov · joined by artifact · Palomar

Read formalization.yaml

authors
Terence Tao
method
agent — Claude Opus 5 (Anthropic)
review
self-assessed (Terence Tao)
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
results
2 main results named, checked with Comparator, with an alignment table
sources
A digestion of the proof of Sendov's conjecture — formalizes; Research Problems in Function Theory (statement of Sendov's conjecture) — background; Some properties of extremal polynomials for the Ilieff conjecture — formalizes; On a problem of Ilyeff — background
related
https://www.proofatlas.ai/formalizations/sendov-conjecture/ — builds-on
divergences
Faithful to the source, and in two respects stronger than it. The blog post argues Sendov's conjecture for n >= 5; this development proves all n >= 2, adding degrees 2 to 4 in Sendov/Analytic/LowDegree.lean. The blog post states the non-strict conclusion; this development additionally extracts the Phelps-Rodriguez equality classification, strengthening the distance bound to a strict inequality except for p = c(z^n - a^n) with |a| = 1. Both are generalizations rather than weakenings: no hypothesis of the source was strengthened, and no part of its statement was dropped. One step is proved by a different route than the informal account: for n >= 101 the write-up in docs/proof-large-degree.md splits 0 <= alpha <= 17 at alpha = 16 and estimates the two pieces by exact rational endpoint bounds, whereas Sendov/LargeDegree/Endgame.lean settles the whole interval with one generated Bernstein certificate, Sendov.F_pos, which the sharp Beta constant leaves enough margin for. The conclusion is the same. Lemma names differ from the informal text throughout; the roadmap in README.md records the correspondence.
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Formal material

Formal statements · 1
Cited proofs · 1
Also known as · 2
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Sendov.lean
  • FormalConjectures/Wikipedia/Sendov.lean