VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
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$.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra (pre-release)
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.
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.
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$.
Known method families
construction (source-reported)
Source-reported tools: construction.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
The source status is candidate and must not be represented as solved.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.