Smale's conjecture with the optimal constant $\frac{d-1}{d}$

Open

SmaleMeanValue.smale_mean_value_conjecture_optimal

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisopen-problempolynomials

Let $P$ be a complex polynomial of degree $d \ge 2$ and let $z \in \mathbb C$ with $P'(z) \neq 0$ . Then there is a critical point $c$ of $P$ with

\left| \frac{P(z) - P(c)}{z - c} \right| \le \frac{d-1}{d}\,|P'(z)|.

This is the strong form of Smale's conjecture, with the constant that the example $z^d - dz$ shows to be optimal in each degree. It implies the goal ( $K = 1$ ) and is open; Tischler proved it for polynomials with only real roots and for polynomials whose roots all have the same absolute value.

Preamble

import Mathlib
open Polynomial

Formal statement

namespace SmaleMeanValue

theorem smale_mean_value_conjecture_optimal (P : ℂ[X]) (hP : 2 ≤ P.natDegree) (z : ℂ)
    (hz : P.derivative.eval z ≠ 0) :
    ∃ c : ℂ, P.derivative.eval c = 0 ∧
      ‖(P.eval z - P.eval c) / (z - c)‖ ≤
        (((P.natDegree : ℝ) - 1) / P.natDegree) * ‖P.derivative.eval z‖ := by sorry

end SmaleMeanValue

Source

Wikipedia, "Mean value problem", revision oldid=1374678764, https://en.wikipedia.org/w/index.php?title=Mean_value_problem&oldid=1374678764, lead section and section "Partial results" (the optimal bound K = (d-1)/d); Tischler (1989); Smale (1981)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

Disclosure — NOT an independent read-back. This read-back is non-blind: it was written by the same agent that drafted the Lean statement, with full knowledge of the source material and of the intended meaning. It must not be treated as independent testimony. Reviewers should compare the Lean code against the source themselves.

Let $P$ be any polynomial with complex coefficients, and write $d$ for its degree (the natural-number degree; for the zero polynomial this would be $0$ , but here it is excluded because $d \ge 2$ is assumed). Write $P'$ for the formal derivative of $P$ and $P(w)$ for evaluation at $w \in \mathbb C$ . Let $z$ be any complex number such that $P'(z) \neq 0$ . The statement asserts that there exists $c \in \mathbb C$ with $P'(c) = 0$ and

\left| \frac{P(z) - P(c)}{z - c} \right| \le \frac{d-1}{d}\,|P'(z)| ,

where $\frac{d-1}{d}$ is computed in the real numbers from $d$ (so it lies in $[\tfrac12, 1)$ for $d \ge 2$ ). Here $c$ ranges over all complex numbers; the condition $P'(c) = 0$ says that $c$ is a critical point of $P$ . Because $P'(z) \neq 0$ and $P'(c) = 0$ , necessarily $c \neq z$ , so the denominator $z - c$ is never zero and no division-by-zero convention is involved. The absolute values are the usual modulus on $\mathbb C$ . No hypotheses on the roots of $P$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Smale's conjecture with the optimal constant d−1d\frac{d-1}{d}dd−1​

Smale's conjecture with the optimal constant $\frac{d-1}{d}$