--- id: "2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra" url: "https://postcutoff.com/e/2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra/" as_of: "2026-10-16T12:39:00+02:00" date: "2026-09-03" date_precision: day category: science importance: 4 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 5 editor: human editor human_review: null version: "2026-10-16" --- As of: 2026-10-16 12:39 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra/ # GPT-6 Astra autonomously disproves Smale's mean value conjecture in Lean Full title: GPT-6 Astra autonomously disproves Smale's mean value conjecture (constant 1) in Lean; HKU mathematicians build on it to show Smale's constant exceeds 1.1018 In an Epoch AI LeanOpenProblems evaluation run in September 2026, a pre-release GPT-6 Astra autonomously produced a Lean 4 proof that Smale's mean value conjecture with constant 1 is false: there is a polynomial p with p(0) = 0, p'(0) = 1 and |p(c)/c| > 1 at every critical point c. Tom Adamczewski published the proof (GitHub repository created 3 Sep 2026); MathWorld lists it as a proposed counterexample. On 15 Oct 2026 Aneesh Jatar and Tuen-Wai Ng (University of Hong Kong) posted arXiv 2610.21472, which builds on the Astra construction, recasts Smale's question in univalent function theory and proves Smale's constant M > 1.1018, with polynomials of arbitrarily large degree beating 1.1018. ## Key facts - Conjecture: Smale (1981) proved that every polynomial has a critical point c with |p(z) − p(c)|/|z − c| ≤ 4|p'(z)|, and asked whether 4 can be replaced by 1 (or by (d−1)/d); one of Smale's problems for the 21st century. Known for degree d ≤ 4 and special classes - Claim: the K = 1 conjecture is false; the witness has 'very large, unspecified degree and violates the bound by a small margin' (repository README) - How found (README): Epoch AI evaluation run 'wikipedia-vega-1000usd' of its LeanOpenProblems harness; a pre-release GPT-6 Astra attempted all 222 research-open statements of the Wikipedia collection of Google DeepMind's Formal Conjectures, once each, with $1,000 and 96 hours per statement, in a network-isolated container; 'No human saw or steered the proof search' - Cost (README): about 2.2M output and 68M cache-read tokens, $265 at GPT-6 Astra list prices; 15.0 hours of agent working time - Verification: Lean 4 + Mathlib proof checked by Comparator against the Formal Conjectures statement, using only propext, Quot.sound and Classical.choice; the README's prose account of the proof is machine-generated and 'has not been checked by a human mathematician' - Construction (README): a conformal map of the four-petal set {|z⁴ + 64i| ≤ √4097}, a Blaschke factor, polynomial approximation, then adding the primitive of q²ⁿ pushes all critical points into a thin collar where |g| > 1 + δ - MathWorld (last updated 2 Oct 2026): 'Adamczewski (2026) released a proposed counterexample to the constant 1, constructed autonomously by GPT-6 Astra'; independent review 'had not been reported as of Sep. 7, 2026' - Human follow-up: Jatar & Ng, 'Smale's mean value constant and admissible univalent Blaschke pairs', arXiv 2610.21472 (15 Oct 2026): 'Motivated and based upon the GPT-6 Astra construction'; they show M = A = B (two new extremal constants) and 1.1018586788… = √(8081/6656) ≤ B₁ < √(7/5), so M > 1.1018. The original argument can give S(P) > 1 + 2⁻³⁵ but is 'hard to push' further - AI use in the follow-up: 'GPT-6Astra and Grok 4.6 were utilized to conduct numerical experiments and generate preliminary draft proofs via targeted prompting. The authors then collaboratively verified, significantly simplified, and rewrote all proofs in their own words.' Tuen-Wai Ng co-authored the 2002 Beardon–Minda–Ng bound on the same problem ## What happened 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.21472](https://arxiv.org/abs/2610.21472). 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. ## Why it matters 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. ## What is disputed or not yet verified - Verification: Formal proof in Lean (Comparator-checked); follow-up is an unrefereed preprint by specialists ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 126 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 65 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 156 days after its cutoff - Grok 4.7 (training cutoff May 2026): 95 days after its cutoff ## Sources 1. [GitHub: tadamcz/mean-value-problem (Lean 4 disproof found by GPT-6 Astra)](https://github.com/tadamcz/mean-value-problem) (github.com, code) 2. [arXiv 2610.21472: Smale's mean value constant and admissible univalent Blaschke pairs (Jatar & Ng)](https://arxiv.org/abs/2610.21472) (arxiv.org, paper) 3. [MathWorld: Smale's Mean Value Conjecture](https://mathworld.wolfram.com/SmalesMeanValueConjecture.html) (mathworld.wolfram.com, docs) 4. [Epoch AI: LeanOpenProblems harness](https://github.com/epoch-research/LeanOpenProblems) (github.com, code) 5. [Formal Conjectures: MeanValueProblem.lean](https://github.com/google-deepmind/formal-conjectures/blob/9cbe1d3c12998c786b7c2cd99ce28a21b6631f66/FormalConjectures/Wikipedia/MeanValueProblem.lean) (github.com, code) ## Changes - 2026-10-16 (filed): Created from the Jatar–Ng arXiv paper, the GitHub repository and MathWorld; the September result had been missed ## Related - 2026-09-10: [GPT-6 Astra's Epoch AI run adds more Lean-checked results](https://postcutoff.com/e/2026-09-10-astra-leanopenproblems-september-results/index.md) - 2026-09-03: [Pre-release GPT-6 Astra disproves Erdős's 'first serious problem' (1931, $500) and proves the rational-exponents conjecture, all Lean-verified, in Epoch's FrontierMath Erdős runs](https://postcutoff.com/e/2026-09-03-frontiermath-erdos-astra-disproves-erdos-problem-1/index.md)