Smale’s Mean Value Conjecture ( $K=1$ )

Smale conjectured that in his mean value theorem for complex polynomials, the universal constant $4$ could be replaced by $1$ . Equivalently, for every complex polynomial $p$ of degree at least $2$ and every $z\in\mathbb C$ , there should exist a critical point $c$ of $p$ such that $\frac{|p(z)-p(c)|}{|z-c|}\le |p'(z)|.$ The conjecture is false: there exists a polynomial $p$ with $p(0)=0$ and $p'(0)=1$ such that $\left|\frac{p(c)}{c}\right|>1$ for every critical point $c$ .

Result: Disproved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Construction
Field: Complex polynomials
Posed by: Stephen Smale
Year posed: 1981
Years open: 45y
Solved: 2026-09-03
Model: GPT-6 Astra (pre-release)
Vendor: OpenAI
Collaborators: Tom Adamczewski
Verification: Lean-verified
Publication: Announced
Significance: 45 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

The formal proof constructs a complex polynomial $p$ such that $p(0)=0,\qquad p'(0)=1,$ and for every critical point $c$ of $p$ , $\left|\frac{p(c)}{c}\right|>1.$ Thus at $z=0$ there is no critical point satisfying $\frac{|p(0)-p(c)|}{|c|}\le |p'(0)|=1,$ which disproves Smale's conjectured universal constant $K=1$ .

The counterexample has very large unspecified degree and violates the bound only by a small margin, so it is consistent with Smale's original $K=4$ theorem, the known low-degree positive cases, and previous asymptotic improvements toward $1$ .

What the AI did

A pre-release GPT-6 Astra autonomously attempted the Formal Conjectures statement in Epoch AI's LeanOpenProblems evaluation. No human saw or steered the proof search. Astra found a new counterexample construction and wrote the Lean proof. The proof builds a holomorphic model on a nonconvex compact set, approximates it polynomially, and adds a high-power perturbation that forces all critical points into a region where the $K=1$ inequality fails. Claude was later used to write repository documentation from the completed run; it was not the mathematical solver.

Verification

Lean-verified on this site's ladder: kernel-checked, and the statement was written independently of the prover. Checked here on 5 September 2026 from a clone of the repository at f99ab98: 2,266 lines of Lean across the development, zero `sorry` outside the Challenge.lean stub, zero `axiom` declarations, no `native_decide`, `unsafe` or `implemented_by`; the mathlib revision is pinned; CI runs Comparator against the trusted statement allowing only propext, Quot.sound and Classical.choice. The compared statement is byte-identical to Formal Conjectures' `mean_value_problem` at commit 9cbe1d3c, which is Smale's K = 1 form exactly: the quantified K is unused there, and the division convention in Lean (x/0 = 0) only makes the conjecture easier to satisfy, so it cannot help a disproof. Candidate rather than resolved because, two days after the run, no mathematician outside it has read the proof; the witness is a nonconstructive limiting perturbation of large unspecified degree and violates the bound by a small margin, which is consistent with everything known. The proof account was machine-generated and is unaudited.

Sources

Lean proofSolution.lean and the Lean development
Lean statementChallenge.lean: the compared statement, copied from Formal ConjecturesFormal Conjectures source statement (Google DeepMind)
CodeGithub
DiscussionX Announcement
OtherEpoch AI LeanOpenProblems, the evaluation the run was part of

Submitted by VibeGene on 04 Sep 2026

Smale’s Mean Value Conjecture (K=1K=1K=1)

What was actually shown

What the AI did

Verification

Sources

Discussion

Smale’s Mean Value Conjecture ( $K=1$ )