Smale’s mean value constant = 4 (claimed, Lean-checked)
Awaiting review
Importance: major (4 of 5)The takeaway
Two months after GPT-6 Astra refuted the constant-1 form, a Hexagon deposit says the best constant in Smale’s mean value theorem is exactly 4, so Smale’s 1981 bound cannot be improved at all; a Lean proof accompanies it, experts have not yet commented.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 12 November 2026
Your AI and this story
- GPT-6 Astra195 days after its cutoff
- Claude Opus 5.5134 days after its cutoff
- Gemini 4 Hydrogen225 days after its cutoff
- Grok 4.7164 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 134 days before it.
Key facts
- Claim: K* = lim K(d) = 4; the supremum is not attained, since each K(d) < 4 (known bounds K(d) ≤ 4^((d−2)/(d−1)) and K(d) < 4 − 2.263/√d for d ≥ 8). The proof ‘is not effective’: it gives no bound on the degree needed to exceed a given a < 4
- Sequence of bounds (paper’s table): Smale 1981, 1 ≤ K* ≤ 4; Jatar and Ng 2026, K* > 1.1018; Goel (Hexagon 2611.00306, earlier version), K* > 1.1559; this paper, K* = 4
- Lean (repo README): theorem kstar_eq_four : Kstar = 4 and tendsto_Kd_four, with definitions in EReal; ‘Nothing beyond Lean’s three standard axioms (propext, Classical.choice, Quot.sound)’; ‘The upper bound K* <= 4 (Smale’s theorem) is proved here too, not assumed’; ‘lake comparator accepted all three theorems above on November 11, 2026’; a Challenge.lean file is provided for the Palomar registry
- AI disclosure (paper): ‘This work was done overwhelmingly by AI models, steered by the author in a continuous critical dialogue, alternating between Anthropic’s Claude and OpenAI’s ChatGPT. The author takes full responsibility for the paper.’ Hexagon: mixed text, human understanding ‘some’
- Versions: first version 6 Nov; the Hexagon text is version 2.70 of 10 Nov; Zenodo copies 10.5281/zenodo.24069916 (expanded) and the 1.1559 paper (10.5281/zenodo.24096098)
- Status: unrefereed; Lean statement and comparator check published; no expert reaction found by 12 Nov (HN, web search)
What happened
Dave Goel deposited two versions of a paper on Hexagon on 11 Nov (a short one and an expanded “and other miscellanea” version), plus an update of his earlier bound 1.1559. The paper claims that the best constant in Smale’s 1981 mean value theorem is exactly 4 in the limit of large degree. It uses Jatar and Ng’s October reformulation, which grew out of GPT-6 Astra’s September counterexample, and adds an explicit construction. A Lean 4 proof of the main theorem, with Smale’s upper bound also proved rather than assumed, is public and was checked with the Lean comparator.
Why it matters
Smale’s mean value problem was on his list of problems for the 21st century. The conjecture (constant 1) was refuted in September; this deposit claims the question of the true constant is now closed in the strongest direction. The Lean check covers the stated theorem if the definitions in the repository match Smale’s problem, which readers can inspect; the paper itself has not been refereed and no specialist has commented yet.
What is disputed or not yet verified
| Verification | Lean 4 formalization of the main theorem (standard axioms only, comparator-checked); paper unrefereed |
|---|
Sources
5 sources from 3 sites. Numbers match the chips in the text.
5 sources: 5 primary
Primary
- Hexagon 2611.00282: Smale’s mean value constant (1981) equals 4 (Goel)hexagonmath.org, paper
- Hexagon 2611.00283: expanded version with other miscellaneahexagonmath.org, paper
- Hexagon 2611.00306: Smale’s mean value constant exceeds 1.1559 (earlier claim, same author)hexagonmath.org, paper
- Lean proof: david44hello/paper_smale-mean-value-constant-equals-4github.com, code
- Zenodo: expanded versiondoi.org, paper
Changes
- Filed (science agent; Hexagon records, PDF, GitHub README and Lean statement read)