Formally verified Autonomous

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.

Lab: OpenAI / Epoch AI
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

GitHubtadamcz/mean-value-problem, the Lean 4 disproof↗

Independent commentary

VibeMathedSmale's mean value conjecture (K = 1)↗

What was found

Smale proved in 1981 that for every complex polynomial $f$ of degree at least two and every point $z$ there is a critical point $c$ with $|f(z) - f(c)|/|z - c| \le K|f'(z)|$ for $K = 4$ , and asked whether $K$ can be lowered to 1. 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 was claimed until 2026-09-24 because no third party had audited the statement against the literature. That audit now exists twice, by vibemathed and by this registry, and both find the compared statement to be the negation of Formal Conjectures' mean_value_problem verbatim, a statement written independently of the prover, so the grade is formal. The formal grade certifies the disproof, not the machine-generated proof account, which no mathematician outside the run has read. 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.

Independent checks

vibemathed.com statement audit: From a clone at f99ab98: the compared statement is byte-identical to Formal Conjectures' mean_value_problem at 9cbe1d3c, with no sorry outside the challenge stub, no axiom declarations and no native_decide, and CI runs Comparator permitting only the three standard axioms. · link ↗

whataifound.org (statement comparison): Compared Challenge.lean at commit 15e07155 with the Formal Conjectures file at 9cbe1d3c: the compared theorem is the negation of mean_value_problem with identical hypotheses and inequality. At that commit the repository's Lean build and statement-against-solution CI jobs pass; the one failing job checks a README link. · link ↗

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.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

History of this entry

2026-09-24RegradedUpgraded from claimed to formally verified: the compared statement was audited against the literature, by vibemathed and here, and is Formal Conjectures' formalization verbatim, which clears the only reason the entry gave for withholding the formal grade. source ↗
2026-09-15AddedEntered the registry graded Formally verified and Autonomous.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Graded formally verified for verification and autonomous for autonomy. What these mean.

Cite this entry

Plain text

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-k1

BibTeX

@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: Formally verified. Autonomy: Autonomous.},
  url          = {https://whataifound.org/finding/2026-09-03-smale-mean-value-k1}
}

Related findings

Formally verifiedSendov's conjecture proved for every degreeIndependent · 2026-08-05 Author verifiedA 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin familiesIndependent · 2026-09-09 ClaimedDisproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequencesOpenAI / Epoch AI · 2026-09-05

complex-analysis polynomials lean formalization construction

← All mathematics findings in the registry