Global regularity of smooth solutions to the 3D incompressible Euler equations

### What is the conjecture

The incompressible Euler equations in three spatial dimensions are given by:
$$\frac{\partial u}{\partial t} + (u \cdot \nabla) u + \nabla p = 0$$
$$\nabla \cdot u = 0$$

where $u: \mathbb{R}^3 \times [0,T) \to \mathbb{R}^3$ is the velocity field and $p: \mathbb{R}^3 \times [0,T) \to \mathbb{R}$ is the pressure field.

**The Problem:** Given a smooth divergence-free initial velocity field $u_0 \in C^\infty(\mathbb{R}^3, \mathbb{R}^3)$ with finite kinetic energy (i.e., $\|\nabla u_0\|_{L^2(\mathbb{R}^3)} < \infty$), does there exist a unique classical solution $u$ that remains smooth for all time $t > 0$?

In two spatial dimensions, the answer is affirmative (Wolibner, Hölder). In three dimensions, this is a fundamental open problem. The main obstruction is vortex stretching: the vorticity $\omega = \nabla \times u$ satisfies $\frac{\partial \omega}{\partial t} + (u \cdot \nabla) \omega = (\omega \cdot \nabla) u$, where the nonlinear stretching term $(\omega \cdot \nabla) u$ can potentially cause finite-time blowup.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Euler_equations_(fluid_dynamics), https://arxiv.org/abs/1904.08385, https://terrytao.wordpress.com/2018/10/09/254a-notes-3-local-well-posedness-for-the-euler-equations/, https://users.cms.caltech.edu/~hou/papers/Acta_Num_Hou_09.pdf, https://cscamm.umd.edu/publications/euler_CS-04-07.pdf

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-03-08)

Building blocks (1-3; from search results):
- Vector field calculus and differential operators ($\nabla$, divergence, curl)
- Sobolev spaces and function spaces for PDEs
- PDE theory for existence and uniqueness of solutions

Missing pieces (exactly 2; unclear/absent from search results):
- A comprehensive formalization of incompressible fluid dynamics, including the vorticity formulation and vortex stretching dynamics
- Theory for global well-posedness of nonlinear PDEs with the specific structure of the Euler equations (advection plus stretching term)

Rating justification (1-2 sentences): Mathlib has foundational analysis and functional analysis, but lacks specific infrastructure for formulating and analyzing the 3D incompressible Euler equations. Significant new definitions would be needed to properly state the problem and key results like the Beale-Kato-Majda criterion.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-35
* ams-76

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

If you have feedback on mistakes / hallucinations, feel free to just write it in the issue. See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Start by reading the cited Euler-equation sources and the issue's prerequisites to establish the precise conjecture and its assumptions. Check whether the required vector calculus, Sobolev-space, PDE, and incompressible-fluid infrastructure exists; done means the conjecture is added to the repository as a formal statement.

Written by the indexing model from the issue text.