Skip to content

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

@franzhusch

Description

@franzhusch

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:

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

  • ams-35
  • ams-76

Choose either option

  • I plan on adding this conjecture to the repository
  • 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

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions