Theorem · version 3
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.
This less detailed formal nonexistence statement is distinct from the explicit compact-data maximal-lifespan theorem.
This source presents a theorem with a proposed proof. Its wording does not establish acceptance or independent mathematical review.
Proposed
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
Replaces an earlier source assessment. Version history ↓
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
Euler.euler_breakdown_R3Commit f9e8bc5b38b6e212696e8a30e3e91517af887bbd
In this problem · publication v7 · Selected context
Supporting result · Proposed
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v9
Supporting result · Proposed
Relationship not independently reviewed. This concerns its use in this problem.
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
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.
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.
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.
Exact proof source inspected. This digest identifies this file only, not a project build, theorem correspondence or independent reproduction.
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.
Euler nonexistence and compact-data proofs: f9e8bc5b38b6e212696e8a30e3e91517af887bbd.
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proposed
The distinct, less detailed formal endpoint.
Source dated Sep 8, 2026 · Observed Oct 13, 2026 · Source passage →
Replaces an earlier source assessment; see the original source for its history.