Partial differential equations · Mathematical physics · Question
Three-dimensional Euler regularity
Can smooth compactly supported initial velocity form a finite-time singularity in the three-dimensional incompressible Euler equations without external forcing?
ProposedOpenMath assessment · Oct 13, 2026
- Literature: 1 published paper · 1 preprint · 2 projects
- Formal: 2 complete proofs
- Computation: None recorded
- Review: Not yet reviewed
Frontier 1 report →
Earlier version 8 of this page. View current →
Overview
Current assessment
OpenAI reports finite-time breakdown from smooth compactly supported unforced Euler data, with a detailed formal theorem. The new proof and statement correspondence are under assessment.
Open questions
The mathematical target is finite-time breakdown from the stated smooth compactly supported unforced data. Forced, bounded-domain and lower-regularity results have different hypotheses.
Latest
Precise statement
Velocity u and pressure p satisfy and div u = 0 on ℝ³. There is no viscosity and no external force. The selected question uses smooth divergence-free compactly supported initial velocity, the maximal smooth lifespan T*, and growth of velocity derivatives/vorticity. Lower-regularity data, bounded domains and forced Euler are different scopes.
Definitions
- Incompressible and unforced
- The velocity has zero divergence and the equation has no external force. These conditions distinguish this question from forced singularity constructions.
Question paraphrased by OpenMath. Original wording is available in the sources.
Landscape
Figures and explorable examples. Selecting a statement opens its exact wording.
Visual setup
Smooth data, unforced evolution, a breakdown diagnostic
The question begins with smooth compactly supported velocity. No force or viscosity is present; a singularity is diagnosed by derivative and integrated-vorticity growth.
Reading boundary. No curve, color or arrow is numerical evidence of blowup. The schematic does not represent an actual velocity field or a certified computation.
Inspect the smooth-data singularity statement◌ ProposedCompare global nonexistence◌ ProposedRead the vorticity continuation criterion● Proved under stated assumptions
Select a statement to compare its regularity, lifespan and evidence. The arrows explain the setup only.
Results
The question 1
- ProposedSmooth unforced data with finite-time breakdownOpenAI 2026Formalized
The 2026 manuscript’s smooth-data theorem; the source-reported formal proof is under mathematical assessment.
Theorem · Primary formulation
ProposedOpenAI 2026Smooth unforced data with finite-time breakdown
There exists smooth compactly supported divergence-free initial velocity on ℝ³ whose unforced incompressible Euler solution has a positive finite maximal smooth lifespan T*, with limsup as t ↑ T* of ‖∇u(t)‖∞ infinite and infinite.Assumptions
- Three-dimensional whole-space incompressible Euler.
- No external force and no viscosity.
- Initial velocity is smooth, compactly supported and divergence-free.
- Equation
- Unforced inviscid Euler on ℝ³; ν = 0
- Initial data
- Smooth, compactly supported and divergence-free
- Conclusion
- Smooth finite-time singularity
In this problem
The 2026 manuscript’s smooth-data theorem; the source-reported formal proof is under mathematical assessment.
Formal proofs
- Lean: compact smooth Euler singularity ↗Complete formal proof reported externally
Sources
Proposed 1
- ProposedNo global smooth bounded-energy solution for selected dataOpenAI 2026Formalized
This less detailed formal nonexistence statement is distinct from the explicit compact-data maximal-lifespan theorem.
Theorem · Supporting result
ProposedOpenAI 2026No global smooth bounded-energy solution for selected data
There exists smooth rapidly decaying divergence-free initial velocity on ℝ³ for which no global smooth unforced incompressible Euler velocity and pressure with uniformly bounded kinetic energy exist.Assumptions
- The whole-space decay and bounded-energy solution predicates in the cited formal project.
- No viscosity or external force.
- Equation
- Unforced inviscid Euler on ℝ³; ν = 0
- Initial data
- Smooth, rapidly decaying and divergence-free
- Conclusion
- No global smooth solution with uniformly bounded kinetic energy
In this problem
This less detailed formal nonexistence statement is distinct from the explicit compact-data maximal-lifespan theorem.
Formal proofs
- Lean: unforced whole-space nonexistence ↗Complete formal proof reported externally
Sources
Conditional implications 1
- ProvedFinite-time smooth breakdown requires divergent integrated vorticityBeale et al. 1984
Beale–Kato–Majda is a conditional criterion; it does not itself construct a singularity.
Theorem · Conditional implication
ProvedBeale et al. 1984Finite-time smooth breakdown requires divergent integrated vorticity
For an unforced three-dimensional Euler solution in the classical Sobolev class , , a finite maximal smooth lifespan T* requires . In particular, a finite value of this integral allows smooth continuation past that time.Assumptions
- Classical divergence-free Euler solution on ℝ³ in H^s with s > 5/2.
- The solution is smooth up to each earlier time and the continuation criterion applies.
- Equation
- Unforced inviscid Euler
- Initial data
- Classical divergence-free solution on ℝ³ in H^s, s > 5/2
- Conclusion
- A vorticity-integral continuation criterion; not a blowup construction
In this problem
Beale–Kato–Majda is a conditional criterion; it does not itself construct a singularity.
Sources
Compare statements · 3
Each row is a separate assertion. Its assumptions determine which question it answers.
| Statement | Equation | Initial data | Conclusion |
|---|---|---|---|
| Smooth unforced data with finite-time breakdown → Proposed Exact statement & sources | Unforced inviscid Euler on ℝ³; ν = 0 | Smooth, compactly supported and divergence-free | Smooth finite-time singularity |
| No global smooth bounded-energy solution for selected data → Proposed Exact statement & sources | Unforced inviscid Euler on ℝ³; ν = 0 | Smooth, rapidly decaying and divergence-free | No global smooth solution with uniformly bounded kinetic energy |
| Finite-time smooth breakdown requires divergent integrated vorticity → Proved Exact statement & sources | Unforced inviscid Euler | Classical divergence-free solution on ℝ³ in H^s, s > 5/2 | A vorticity-integral continuation criterion; not a blowup construction |
No global smooth bounded-energy solution for selected data →
Finite-time smooth breakdown requires divergent integrated vorticity →
Connections
Consequences 1
Assuming Smooth unforced data with finite-time breakdownProposed
A singularity must defeat the vorticity continuation criterion
ConditionalIf the reported smooth-data construction is valid, its divergent integrated vorticity provides the expected classical breakdown diagnostic.
Limit A large finite vorticity value or a finite numerical trajectory does not establish the required divergence.
Sources & review
For an unforced three-dimensional Euler solution in the classical Sobolev class , , a finite maximal smooth lifespan T* requires . In particular, a finite value of this integral allows smooth continuation past that time.
Beale–Kato–Majda is a conditional criterion; it does not itself construct a singularity.
- Remarks on the Breakdown of Smooth Solutions for the 3-D Euler Equations ↗Communications in Mathematical Physics 94 (1984), 61–66; criterion also recalled in the 2026 manuscript Section 1.1
- Finite Time Blowup for the Euler Equation ↗Theorem 1.1 and Section 1.1
Source-grounded explanation · independent explanation review: pending.
Approaches
How the problem is attacked, and what each line of attack cannot yet reach.
Transfer amplification across localized oscillation scales
The manuscript iterates localized oscillations over smooth Euler flows and chooses scales to accumulate a finite-time breakdown.
Cannot yet reach The diagram names hypotheses and diagnostics; it does not depict the constructed velocity field or solve the PDE.
Sources & review
Supporting statements
- Finite Time Blowup for the Euler Equation ↗Theorem 1.1 and Section 1.1
Source-grounded explanation · independent explanation review: pending.
Timeline
Two distinct Euler formal theoremsFormalization
The pinned revision exposes both nonexistence and detailed compact-data singularity statements.
Formal source completion is reported externally; OpenMath has not reproduced the build.
- Smooth unforced data with finite-time breakdownProposed
- No global smooth bounded-energy solution for selected dataProposed
- Navier–Stokes and Euler formal proof sources ↗formalization.yaml; exact main declarations and Comparator instructions
- Navier–Stokes and Euler formal proof sources ↗Euler/Solution.lean: exists_compact_smooth_euler_singularity
- Navier–Stokes and Euler formal proof sources ↗Euler/Solution.lean: euler_breakdown_R3
A smooth unforced whole-space construction is releasedProposal
OpenAI releases the Euler manuscript and formal source alongside the viscous work.
The announcement credits separate concurrent forced-Euler work to Alpöge and Buckmaster; its scope differs.
- Finite Time Blowup for the Euler Equation ↗Theorem 1.1 and Section 1.1
- On the Navier–Stokes Millennium Prize Problem ↗Our process; concurrent work; Euler and Navier–Stokes scope
A vorticity continuation criterionRelated result
Beale, Kato and Majda identify integrated maximum vorticity as a continuation diagnostic.
The criterion constrains possible breakdown; it is not an existence construction.
- Remarks on the Breakdown of Smooth Solutions for the 3-D Euler Equations ↗Communications in Mathematical Physics 94 (1984), 61–66; criterion also recalled in the 2026 manuscript Section 1.1
- Finite Time Blowup for the Euler Equation ↗Theorem 1.1 and Section 1.1
Regularity and boundary conditions matterFoundation
Earlier constructions discussed in the manuscript use lower-regularity data, forcing or different domains.
Their conclusions must not be relabeled as smooth compact-data whole-space unforced blowup.
- Finite Time Blowup for the Euler Equation ↗Theorem 1.1 and Section 1.1
Evidence
| Literature | 1 published paper · 1 preprint · 2 projects Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | Reported in sources: The pinned project reports both a detailed compact-data finite-lifespan theorem and a separate global bounded-energy nonexistence theorem, with zero sorry and standard logical axioms. Their statements were compared; independent review and external build remain pending. |
| Computation | None recorded |
| Review | Not yet reviewed OpenMath assessment: OpenAI reports finite-time breakdown from smooth compactly supported unforced Euler data, with a detailed formal theorem. The new proof and statement correspondence are under assessment. Source comparison and reader curation; independent mathematical assessment remains pending. OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027 Collection last checked Oct 13, 2026. |
Formalizations
Smooth unforced data with finite-time breakdown →
Lean: compact smooth Euler singularityComplete formal proof reported externally
Complete formal proof reported externally
This formal theorem supplies compact support, a maximal lifespan 0 < T* ≤ 1 in the all-order Sobolev class, bounded energy before breakdown, infinite C¹ limsup and divergent integrated vorticity. The project reports only standard logical axioms and self-assessed correspondence. It is not an OpenMath execution.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Euler.exists_compact_smooth_euler_singularityCommit f9e8bc5b38b6e212696e8a30e3e91517af887bbd
No global smooth bounded-energy solution for selected data →
Lean: unforced whole-space nonexistenceComplete formal proof reported externally
Complete formal proof reported externally
This formal theorem excludes a global smooth uniformly bounded-energy solution. It is kept separate from the stronger compact-data finite-lifespan theorem, so the former is not used alone to claim all of the latter’s details.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Euler.euler_breakdown_R3Commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Sources
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Start here
- Introduction
Remarks on the Breakdown of Smooth Solutions for the 3-D Euler Equations →Read the setting and notation before comparing the results.
- Proof source
Finite Time Blowup for the Euler Equation →Read the mathematical argument; inspect its statement for assessment and scope.
- Formal source
Navier–Stokes and Euler formal proof sources →Inspect the formal statement, assumptions and reported checks.
Bibliography 4
- Finite Time Blowup for the Euler Equation →
OpenAI · Preprint · Sep 8, 2026
Theorem 1.1 and Section 1.1
- Navier–Stokes and Euler formal proof sources →
OpenAI · Project documentation · Sep 8, 2026
formalization.yaml; exact main declarations and Comparator instructions
- On the Navier–Stokes Millennium Prize Problem →
OpenAI · Project documentation · Sep 8, 2026
Our process; concurrent work; Euler and Navier–Stokes scope
- Remarks on the Breakdown of Smooth Solutions for the 3-D Euler Equations →
J. Thomas Beale · Tosio Kato · Andrew Majda · Published · 1984
Communications in Mathematical Physics 94 (1984), 61–66; criterion also recalled in the 2026 manuscript Section 1.1
Research activity · 1 entry
Research direction
Keep the concurrent forced result distinct
The announcement recognizes Levent Alpöge and Tristan Buckmaster’s separately generated forced-Euler work with an internal Anthropic model.
No theorem of that separate work is republished here without its own exact source and hypotheses.
Related statements · context, not additional proved progress
On the Navier–Stokes Millennium Prize Problem · sources & artifacts →
Selected literature; source observations and coverage limits are retained in the publication details.
Contributors
OpenAI is the printed author of the unforced Euler manuscript and credits its internal research-model workflow. GPT-6 Astra/Codex is credited for the later formalization. Beale, Kato and Majda own the older continuation criterion. The announcement separately recognizes Levent Alpöge and Tristan Buckmaster’s Anthropic-assisted forced-Euler result; it is not the same unforced theorem. Individual mathematical checking roles are not inferred from formal code.
Authors & roles
Finite Time Blowup for the Euler Equation →
OpenAI
OpenAI attributes the argument to its internal research model. Bibliographic authorship is printed as OpenAI; individual human preparation and checking roles are not inferred.
Navier–Stokes and Euler formal proof sources →
OpenAI
The project metadata names GPT-6 Astra with Codex for formalization and marks alignment review as self-assessed. Lean, Mathlib and independent statement/Comparator infrastructure have separate supporting roles.
On the Navier–Stokes Millennium Prize Problem →
OpenAI
OpenAI reports an internal multi-agent research-model workflow and later GPT-6 Astra formalization. It recognizes Alpöge and Buckmaster’s concurrent forced-Euler work, which is distinct from its unforced Euler result.
Remarks on the Breakdown of Smooth Solutions for the 3-D Euler Equations →
J. Thomas Beale · Tosio Kato · Andrew Majda
No specific AI contribution is attributed by this source record.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.
Record details
- Record version
- 8
- Classification
- MSC2020 35Q31 / 76B03
- Prerequisite level
- specialist
Independently assess the reported smooth-data construction and its formal correspondence.
Source observations & version history →