Sendov's conjecture

DefinitionAdmissible radius in Sendov's problem#✓fully proved

A real number \(R\) is an admissible radius if \(R > 0\) and, for every integer \(n \ge 2\) and every complex polynomial \(f\) of degree \(n\) whose zeros all lie in the closed unit disk \(|z| \le 1\), every zero \(\lambda\) of \(f\) has a critical point within distance \(R\), that is, a zero \(c\) of the derivative \(f'\) with \(|c - \lambda| \le R\).

def IsAdmissibleRadius (R : ℝ) : Prop :=
  0 < R ∧
    ∀ n : ℕ, 2 ≤ n →
      ∀ f : Polynomial ℂ, f.natDegree = n →
        (∀ z : ℂ, f.eval z = 0 → ‖z‖ ≤ 1) →
          ∀ lambda0 : ℂ, f.eval lambda0 = 0 →
            ∃ c : ℂ, f.derivative.eval c = 0 ∧ ‖c - lambda0‖ ≤ R

Used by 4

Used byThe admissible radii are bounded below · Enlarging an admissible radius · The Sendov radius · Admissible radii bound the Sendov radius

TheoremEnlarging an admissible radius#✓fully proved

If \(R\) is an admissible radius and \(R \le S\), then \(S\) is an admissible radius.

theorem IsAdmissibleRadius.mono {R S : ℝ} (hR : IsAdmissibleRadius R) (hRS : R ≤ S) :
    IsAdmissibleRadius S

Uses 1

Statement usesAdmissible radius in Sendov's problem

DefinitionThe Sendov radius#✓fully proved

The Sendov radius is the infimum, as a real number, of the set of admissible radii in Sendov's problem.

By the convention for infima of real numbers, it would be \(0\) if no radius were admissible.

noncomputable def sendovRadius : ℝ :=
  sInf {R : ℝ | IsAdmissibleRadius R}

Uses 1 · Used by 4

Statement usesAdmissible radius in Sendov's problem

Used byLower bound one for the Sendov radius · Sendov's conjecture · Admissible radii bound the Sendov radius · Upper bound two for the Sendov radius

TheoremThe admissible radii are bounded below#✓fully proved

The set of admissible radii is bounded below.

Zero is a lower bound, since every admissible radius is positive.

theorem bddBelow_admissibleRadii : BddBelow {R : ℝ | IsAdmissibleRadius R}

Uses 1 · Used by 1

Statement usesAdmissible radius in Sendov's problem

Used byAdmissible radii bound the Sendov radius

TheoremAdmissible radii bound the Sendov radius#✓fully proved

If \(R\) is an admissible radius, then the Sendov radius is at most \(R\).

theorem sendovRadius_le_of_isAdmissibleRadius {R : ℝ} (hR : IsAdmissibleRadius R) :
    sendovRadius ≤ R

Uses 3

Statement usesAdmissible radius in Sendov's problem · The Sendov radius

Proof usesThe admissible radii are bounded below

DefinitionSendov's conjecture#✓fully proved

Sendov's conjecture is the proposition that the Sendov radius is at most \(1\).

def sendovConjecture : Prop :=
  sendovRadius ≤ 1

Uses 1 · Used by 1

Statement usesThe Sendov radius

Used bySendov's conjecture holds

DefinitionLower bound one for the Sendov radius#✓fully proved

This is the proposition that the Sendov radius is at least \(1\).

The polynomials \(z^n - 1\) with \(n \ge 2\) give this lower bound.

def lowerBoundOne : Prop :=
  1 ≤ sendovRadius

Uses 1

Statement usesThe Sendov radius

DefinitionUpper bound two for the Sendov radius#✓fully proved

This is the proposition that the Sendov radius is at most \(2\).

The geometric bound from the Gauss–Lucas theorem gives this upper bound.

def upperBoundTwo : Prop :=
  sendovRadius ≤ 2

Uses 1

Statement usesThe Sendov radius

TheoremSendov's conjecture holds#●ready to prove

Sendov's conjecture is true: the Sendov radius is at most \(1\).

Sendov's conjecture was resolved in 2026 by Lech Mazur's computer-assisted proof.

public theorem_wanted sendovConjecture_holds : sendovConjecture

Sources

• Lech Mazur, A Computer-Assisted Proof of Sendov's Conjecture, ProofAtlas, August 5, 2026, https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf; teorth/sendov, Sendov's conjecture in Lean, https://github.com/teorth/sendov/blob/1ddea92d89f951a0a7cbbffa6c267cf7e6640b1d/Sendov/Conjecture.lean.

Uses 1

Statement usesSendov's conjecture

8 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.