Proposed
Global smooth finite-energy nonexistence reported ↗
The distinct, less detailed formal endpoint.
Navier–Stokes and Euler formal proof sources · Euler/Solution.lean: euler_breakdown_R3 →
Source dated Sep 8, 2026 · Observed Oct 13, 2026
Theorem · version 1
No global smooth bounded-energy solution for selected data
Earlier version 1. View current version 3 →
Statement
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.
Scope
This less detailed formal nonexistence statement is distinct from the explicit compact-data maximal-lifespan endpoint.
This source presents a theorem with a proposed proof. Its wording does not establish acceptance or independent mathematical review.
Evidence
Source reports
Formal proofs
Lean: unforced whole-space nonexistence ↗
Complete formal proof reported externally
This endpoint excludes a global smooth uniformly bounded-energy solution. It is kept separate from the stronger compact-data finite-lifespan endpoint, 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
Connections
In this problem · publication v1 · Selected context
Three-dimensional Euler regularity →
Supporting result · Proposed
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v3
Three-dimensional Euler regularity →
Supporting result · Proposed
Relationship not independently reviewed. This concerns its use in this problem.
Sources
Finite Time Blowup for the Euler Equation →
- Theorem 1.1 and Section 1.1 → · Original passage ↗
Recorded wording
The manuscript states smooth compactly supported unforced Euler data with finite maximal lifespan.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
OpenAI · Preprint · Publication date Sep 8, 2026
Revision & attribution
Source revision: 2026-09-08. Observed Oct 13, 2026.
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 →
- Euler/Solution.lean: euler_breakdown_R3 → · Original passage ↗
Recorded wording
A separate endpoint excludes a global smooth uniformly bounded-energy solution for decaying unforced initial data.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
- formalization.yaml; exact main declarations and Comparator instructions → · Original passage ↗
Recorded wording
The project reports complete main-result formalizations, zero sorry counts and only standard logical axioms at the listed endpoints.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
OpenAI · Project documentation · Publication date Sep 8, 2026
Public formal source; execution and statement correspondence are separate checks.
Navier–Stokes and Euler formal proof sources — pinned source ↗No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Revision & attribution
Source revision: f9e8bc5b38b6e212696e8a30e3e91517af887bbd. Observed Oct 13, 2026.
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.
Navier–Stokes and Euler formal proof sources — pinned source: f9e8bc5b38b6e212696e8a30e3e91517af887bbd.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proposed
Global smooth finite-energy nonexistence reported ↗
The distinct, less detailed formal endpoint.
Source dated Sep 8, 2026 · Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-euler-no-global-smooth-energy-solution
- Statement version
- 1
- SHA-256
- 3ca0534d2674e45fa26f371fbedcc5ad34b182ef7ed004f31e2d96ff41d9b1ca