Counterexample to Smale's mean value conjecture at K = 1
A Lean proof produced in an unsteered benchmark run disproves the K = 1 form of Smale's 1981 mean value conjecture, exhibiting a polynomial for which no critical point meets the bound.
- Model
- GPT-6 Astra (pre-release)
- Field
- Mathematics
- Date
- 2026-09-03
- Human collaborators
- Tom Adamczewski
- Problem posed
- 1981 · open 45 yrs
Sources
Original work
Independent commentary
What was found
Smale proved in 1981 that for every complex polynomial of degree at least two and every point z there is a critical point c with the mean value ratio at most four times the derivative at z, and asked whether four can be replaced by one. The constant has since been lowered to four minus order one over the degree, and the conjecture is known for small degrees and for polynomials whose roots are all real or all of one modulus. This development proves the negation of the Formal Conjectures statement. It came out of the same Epoch AI LeanOpenProblems evaluation run as the Koethe and Erdos-Sos entries already in the registry, and Comparator checks the compared statement against the challenge file under the three standard axioms.
Novelty check
The conjecture dates to 1981 and is one of Smale's problems for the twenty-first century, described as open in the sources the repository cites. No competing counterexample appears in the four registries. The repository's own fidelity note is the substantive part of this check: the compared theorem is the explicit negation of the Formal Conjectures statement, and it observes that Lean's convention that division by zero yields zero makes the formal conjecture weaker than the informal one, so the counterexample refutes the conjecture as stated in the literature rather than only its formalization.
Caveats and known objections
Days old at entry, unrefereed, with no expert in complex analysis on record as having read it. The witness is the weak part and the repository says so: a polynomial of very large unspecified degree that violates the bound by a small margin. That is consistent with Smale's own K = 4 theorem and with the known asymptotics of the best constant, so nothing about it is obviously wrong, but a nonconstructive witness of unspecified degree is hard for a reader to check by hand. The grade is claimed rather than formal because no third party has audited the statement against the literature. Autonomy is autonomous on the same disclosure the Koethe and Erdos-Sos entries rest on: one attempt inside an evaluation harness, with no human seeing or steering the proof search.
Also recorded at
vibemathedsmale-s-mean-value-conjecture-k-1
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Claimed and Autonomous.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded claimed for verification and autonomous for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Counterexample to Smale's mean value conjecture at K = 1. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-09-03-smale-mean-value-k1BibTeX
@misc{whataifound-openai-2026-k1,
title = {Counterexample to Smale's mean value conjecture at K = 1},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI / Epoch AI. Verification: Claimed. Autonomy: Autonomous.},
url = {https://whataifound.org/finding/2026-09-03-smale-mean-value-k1}
}