GPT-6 Astra autonomously disproves Smale’s mean value conjecture in Lean

Smale proved in 1981 that every complex polynomial p of degree at least 2 has, for every point z, a critical point c with |p(z) − p(c)|/|z − c| ≤ 4|p’(z)|. He asked whether 4 can be replaced by 1, or even by (d−1)/d, which the polynomial z − z^d/d attains. In 45 years the constant came down only to 4 − O(1/d). The problem is on Smale’s list of problems for the 21st century.

In September 2026 Epoch AI ran a pre-release GPT-6 Astra over the 222 open statements in the “Wikipedia” collection of Google DeepMind’s Formal Conjectures, once each, with $1,000 and 96 hours per statement. For the mean value problem the model chose the negation and proved it in Lean: there is a polynomial with p(0) = 0 and p’(0) = 1 whose value ratio |p(c)/c| exceeds 1 at every critical point. Tom Adamczewski published the proof with a Comparator check (repository created 3 Sep 2026; the README says the whole repository was machine-written by AI assistants at his direction). The witness has huge, unspecified degree and beats the bound only slightly, which fits all known partial results. MathWorld added it as a “proposed counterexample” and noted that no independent review had been reported as of 7 Sep.

On 15 Oct 2026 Aneesh Jatar and Tuen-Wai Ng of the University of Hong Kong posted arXiv 2610.214722. They describe the Astra construction step by step, say their work is “motivated and based upon” it, and turn Smale’s question into an extremal problem for pairs of a univalent map and a Blaschke product. They prove that Smale’s constant M equals the new constants A and B, and that M > 1.1018 (from B₁ ≥ √(8081/6656)), with polynomials of arbitrarily large degree beating 1.1018. They used GPT-6 Astra and Grok 4.6 for numerical experiments and draft proofs, then “verified, significantly simplified, and rewrote all proofs in their own words”.

No Hacker News thread on the disproof was found (Algolia, 16 Oct); X was not searched.

The conjecture of constant 1 had been the expected answer for decades. Here it was refuted by an unattended benchmark run at about $265 of tokens, with a machine-checked proof, and the result sat in a GitHub repository for six weeks before specialists (one of them an author of a classic bound on the problem) built on it. The Lean proof settles correctness of the formal statement; the follow-up paper is the first expert treatment and is not yet refereed. The stronger (d−1)/d form is also refuted, since it implies the constant-1 form.

Unverified: the exact public release date of the repository (3 Sep is its creation date on GitHub) and whether Epoch AI or OpenAI announced the result.