Contested
3D Navier–Stokes: finite-time blow-up claimed by an OpenAI system
Finite-time blow-up for 3D Navier–Stokes (millennium problem) claimed by an internal OpenAI system
The gist
On September 8, 2026, OpenAI announced that an internal system had shown that the 3D Navier-Stokes equations can "blow up" in finite time, a millennium problem.
DiscoverIA status on October 11, 2026: contested, meaning sourced public objection, with no established refutation.
Text written by an AI, reviewed by Antoine Olivier,
To understand ≈ 30 s reading time, estimated
What it changes
The Navier-Stokes equations describe a viscous, incompressible fluid, and one of the millennium problems asks whether, starting from a smooth state, their solutions always stay smooth in 3D. If the proof held, the answer would be no: a solution that starts smooth would stop being so after a finite time.
What remains unclear
Bastounis, Circelli and Hansen dispute whether the written proof matches its Lean formalisation (Lean is a language in which a computer checks every step of a proof), supplied by OpenAI. A separate dispute, involving Buckmaster and Alpöge, concerns priority, that is who reached the result first. No independent validation or ruling by the Clay Institute is recorded.
In the glossary : Status: disputed
Read the paper
Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs
What it establishes : The authors show that the Lean proof released by OpenAI does not faithfully translate its written proof of finite-time blow-up for Navier-Stokes; they make no claim about whether that proof is correct.
Where to start : The abstract, then Section 3: Examples 3.1 and 3.3 compare bounds in OpenAI's paper with their Lean statements. Section 4 and Theorem A.3 (Appendix A.2) draw a general limit of autoformalisation from them.
Written by an AI · reviewed by a human
For experts
Sources, method, key facts, status history, report an error
Status
Contested
Recorded on · arxiv.org
Outside the verification path
- Announced
- Recordedcontested
- nextTo follow
What this status means
Source reading : Source read word for word (level 3 of 3)
Sourced public objection, with no established refutation.
It stays “Contested” until a refutation is established. It would become “Withdrawn” if its author withdrew it or the reference source marked it incorrect.
Sources
- Main sourceopenai.comlink only, reading not recorded
- Papercdn.openai.comlink only, reading not recorded
- Lean proofgithub.comlink only, reading not recorded
- Disputearxiv.orgpage read word for word
- Disputerits.shanghai.nyu.edupage read through an AI summary
- Disputezenodo.orgpage read through an AI summary
- Claimant's statementopenai.compage read word for word · consulted on Oct 11, 2026 ·
could not have influenced the system in any way
Method
OpenAI publishes a paper (PDF) and a Lean formalisation in the NavierStokesAndEuler repository; the sources read do not describe the mechanism of the claimed blow-up. Bastounis, Circelli and Hansen (arXiv 2610.08144) find that "the formalised Lean proof does not correspond to the NL proof" (NL: natural language); no refutation of the substance is recorded. Status “contested” recorded on October 11, 2026 from arxiv.org (page read, quotation checked word for word).
Limits
The claimant supplies a Lean proof; Bastounis, Circelli and Hansen examined it and conclude that it does not correspond to the natural-language proof.
Key facts
- Claimed by
- OpenAI
announced on Sep 8, 2026 - Nature
- new result
- Field
- Mathematics (PDEs / fluid mechanics)
- Checked by
- claimant; no third party (the Clay Institute has not ruled in the sources read)
- Sources
- 7 : 2 read word for word, 2 through an AI summary, 3 links only
- This entry
- Reviewed by Antoine Olivier, Oct 21, 2026
Status history
Only one observation so far.
- 01
First observation:ContestedCurrent status
contested on whether the Lean matches the text, and on priority; not refuted on substance in the sources read
Source: arxiv.orgread word for word
An observation is added; none is ever erased.
Reactions and objections
- : Navier-Stokes lost in translation : Lean ne garantit pas la correction de la preuve en langage naturel (arxiv.org)
Report an error or suggest a source
Thank you, your message was sent.
Sending failed. Try again, or write to contact@discoveria.ai.
Is your result listed?What each status requires, correcting this entry, replying to it.