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.

Fidelity

How fidelity is graded

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

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

As each project's formalization.yaml states 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.

Something wrong or missing here? Request a correction or add a claim, with its sources.

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

Cite this record

qed.bot, “Sendov's conjecture”, https://qed.bot/s/wikipedia-sendov, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.