Navier–Stokes: unforced Leray–Hopf non-uniqueness, AI-written
Awaiting review
Importance: major (4 of 5)The takeaway
On 6 Nov 2026 three NYU mathematicians deposited on Hexagon an 80-page proof, written mainly by Claude Opus and Codex, that the unforced 3D Navier–Stokes equations have a continuum of Leray–Hopf solutions with the same initial data, following the Jia–Šverák programme. The authors say they understand the broad steps; a Lean formalization is announced but not yet public.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean proof, not yet reviewed
- Importance
- Major (4 of 5)
- Last verified
- 8 November 2026
Your AI and this story
- GPT-6 Astra190 days after its cutoff
- Claude Opus 5.5129 days after its cutoff
- Gemini 4 Argon220 days after its cutoff
- Grok 4.7159 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 129 days before it.
Key facts
- Reactions by 8 Nov: no response from Thomas Hou (whose computer-assisted proof of the unforced case, arXiv 2509.25116, came first) or other experts found by web search
- Claim (abstract): a continuum of distinct suitable weak solutions in the Leray–Hopf class with the same datum; solutions smooth at positive times, satisfying local and global energy equalities, separating in L² at rate t^{1/4+σ}
- Method (abstract): ‘The proof follows the program of Jia and Šverák, with a discretely self-similar background in place of a self-similar one’, built ‘from a train of thin vortex rings’ obtained by lifting a periodic row of planar vortices; a growing Floquet mode is constructed from the angular-two instability of the planar vortex
- AI disclosure (Hexagon provenance, verbatim): ‘Text declaration: Primarily AI-generated. … Some parts of this contribution, but not all, have been checked and understood by a human. … The broad steps of the construction have been understood by the authors.’ Tools: Claude Opus, Codex, Lean
- Lean: ‘Lean formalization forthcoming at the public repository at https://github.com/mcoiculescu/unforced-leray-hopf-public2'; the authors ‘used an adaptation of Scott Armstrong’s skill files for the Lean formalization process’
- Prior work: Albritton–Brué–Colombo proved non-uniqueness for the forced equations (Annals 2022); Hou, Wang and Yang claimed the unforced case with a computer-assisted proof of an unstable self-similar profile (arXiv 2509.25116, v2 March 2026). The Hexagon paper’s bibliography cites Albritton–Brué–Colombo and Guillod–Šverák but, in the parsed list, not Hou–Wang–Yang
- Status: unrefereed deposit, 80 pages, v1 6 Nov; no expert reaction found as of 7 Nov (HN, web search)
What happened
Tristan Buckmaster, Matei Coiculescu and Chen Li deposited the paper on Hexagon on 6 Nov, labelled “no human author claimed” and “primarily AI-generated”. It carries out the Jia–Šverák strategy: find a background solution whose linearization has a growing mode, then build a second solution that branches off it. Here the background is discretely self-similar and is constructed explicitly, so the argument does not depend on numerically certified profiles.
The question was already reported answered: Hou, Wang and Yang (arXiv 2509.25116) gave a computer-assisted proof in 2025–26. The new deposit claims a different and more explicit route, written mainly by AI. The authors say a Lean formalization will follow.
Why it matters
Uniqueness of Leray–Hopf solutions is one of the central questions about the Navier–Stokes equations, alongside (and separate from) the Millennium regularity problem. Buckmaster is a leading figure in fluid non-uniqueness, so the deposit carries weight, but it is unrefereed and only partly checked by its authors.
What is disputed or not yet verified
| Verification | Unrefereed Hexagon deposit; Lean formalization announced, not yet public |
|---|
Sources
4 sources from 3 sites. Numbers match the chips in the text.
4 sources: 4 primary
Primary
- Hexagon 2611.00143: Non-Uniqueness of Leray-Hopf Solutions to the Unforced Three-Dimensional Navier-Stokes Equationshexagonmath.org, paper
- Announced Lean repository (forthcoming)github.com, code
- Hou, Wang, Yang: computer-assisted non-uniqueness for the unforced equations (arXiv 2509.25116)arxiv.org, paper
- Albritton, Brué, Colombo: forced case (arXiv 2112.03116)arxiv.org, paper
Changes
- Re-checked reactions incl. Hou’s: none found
- Filed (science agent; Hexagon record and provenance read; prior Hou–Wang–Yang claim found by web search)