Nonuniqueness with local conservation for the hard-sphere Boltzmann equation

Proves the periodic hard-sphere Boltzmann equation can have two different solutions from the same initial gas.

2 papers September 23, 2026 Explained by AI

The Boltzmann equation describes a thin gas whose molecules fly freely and bounce off each other like billiard balls. DiPerna and Lions showed that solutions exist for very rough starting data, but not that they are unique. One paper builds a starting gas that leads to two different solutions, and Lean, a computer proof checker, has a formal statement of it. A second paper claims the same with exact local conservation of mass, momentum and energy.

First step

1989

Ronald DiPerna and Pierre-Louis Lions, global renormalized solutions of the Boltzmann equation

Significance

Major

It shows that the standard rough-data solution theory for the Boltzmann equation does not fix the future, with a Lean statement.

Trust

Formal proof listed

Field

Partial differential equations

2 papers

The explanation

Picture two hard balls of equal mass. One moves with velocity (1, 0, 0) and one sits still. They touch along the direction ω = (1/√2, 1/√2, 0). The collision rule swaps the part of their relative velocity along ωSource 1. That part has size a = 1/√2, about 0.707. After the bounce, the first ball moves with (1/2, −1/2, 0) and the second with (1/2, 1/2, 0). Total momentum is still (1, 0, 0). The sum of squared speeds, which measures kinetic energy, is still 1. Each collision keeps mass, momentum and energy.

The Boltzmann equation tracks a density F of molecules at each place and velocity. They fly freely and collide in this way. DiPerna and Lions proved that solutions exist for any start with finite mass, energy and entropy. Entropy measures how spread out the gas is. They used renormalized solutions, a weak sense of solving the equation, because the collision term may not even be integrableSource 2. Existence and stability do not give uniquenessSource 3. Uniqueness is known under stronger control, such as bounds by a Gaussian velocity profileSource 4.

The second paper proves nonuniqueness on the three-dimensional torus, a box with opposite faces joined. It builds one starting density with bounded velocities and finite mass, energy and entropy. That start gives two different global renormalized solutionsSource 5. The start has unbounded heights packed into ever smaller regionsSource 6. The idea uses thin cold jets of gas. A jet at scale s can have density about 1/s, but total mass about s²Source 7. With s = 1/2, 1/4, 1/8 and so on, densities reach 2, 4, 8, without limit. Yet total mass stays below 1/4 + 1/16 + 1/64 + …, which is 1/3.

The first paper claims more: both solutions keep exact local conservation of mass, momentum and kinetic energy at every pointSource 8. Earlier weak theories allowed a defect in the momentum and energy balanceSource 9. The obstacles are that thin jets meet their periodic copies and that entropy alone is too weakSource 10. The paper gives each jet a finite lifetime, aims it in an irrational direction, and adds a nearly uniform background gas.

How sure is this? Lean, a computer proof checker, has a formal statement of the second paper's result. It keeps local mass and total momentum, with energy and entropy inequalities. So that result is proved, as far as the Lean statement matches the paper. The exact local conservation version is not in the Lean scope and remains a claim. No specialist review is published.

What it doesn't show. This does not show nonuniqueness for smooth or nearly uniform starting gases, where uniqueness is known. The exact local conservation version is not in the Lean scope.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major, with a Lean statement of the basic nonuniqueness result. The stronger version with exact local conservation is a claim without a Lean check. No specialist review is published.

Words used

Boltzmann equation: An equation for a thin gas whose molecules fly freely and collide in pairs.
Hard spheres: Molecules modelled as billiard balls that bounce elastically when they touch.
Entropy: A number that measures how spread out the gas is; collisions push it one way only.
Renormalized solution: A weak sense of solving the equation, tested through bounded functions of the density.
Torus: A box whose opposite faces are joined, so leaving one face brings you back through the other.
Local conservation: Mass, momentum and energy balance exactly at each point, not only in total.
Maxwellian: The bell-shaped, Gaussian velocity profile of a gas at rest in equilibrium.

The original papers (2)

Nonuniqueness with local conservation for the hard-sphere Boltzmann equation (PDF, opens in a new tab)
October 5, 2026
Nonuniqueness for the periodic hard-sphere Boltzmann equation (PDF, opens in a new tab)
September 23, 2026

Lean notes

All quoted lines (10)

For incoming velocities $v,v_*$ and a collision normal $\omega\in S^2$ , put $a=(v-v_*)\cdot\omega,\qquad v'=v-a\omega,\qquad v_*'=v_*+a\omega.$
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
The need for renormalization is substantive: the stated bounds do not themselves make the quadratic collision term locally integrable.
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
Existence and weak stability do not supply uniqueness.
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
Classical uniqueness theorems impose additional control, such as Maxwellian upper bounds.
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
There is a nonnegative density $F_0$ on $\T^3\times\R^3$ , with bounded velocity support and $\int_{\T^3\times\R^3} F_0(1+|v|^2+|\log F_0|)\dd x\dd v<\infty,$ for which the hard-sphere Boltzmann equation has two distinct global admissible solutions, in the sense of Definition …, with initial datum $F_0$ .
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
Their common datum has bounded velocities but unbounded amplitudes concentrated at successively smaller spatial scales.
Nonuniqueness for the periodic hard-sphere Boltzmann equation Back to text
Its velocity-integrated density can be of order $1/s$ , but its total mass is of order $s^2$ .
Nonuniqueness with local conservation for the hard-sphere Boltzmann equation Back to text
We construct one nonnegative initial density with bounded velocity support and finite mass, energy, and absolute entropy that gives rise to two distinct such solutions.
Nonuniqueness with local conservation for the hard-sphere Boltzmann equation Back to text
The periodic formulation in gives local mass conservation, but allows a nonnegative matrix-valued defect in the momentum balance and a corresponding defect in total energy.
Nonuniqueness with local conservation for the hard-sphere Boltzmann equation Back to text
First, thin jets eventually meet their periodic copies.
Nonuniqueness with local conservation for the hard-sphere Boltzmann equation Back to text

Other sources

openai/math, Lean scope note for family 363 The formalization proves nonuniqueness for the periodic hard-sphere Boltzmann equation by constructing two distinct global renormalized solutions on $\mathbb T^3\times\mathbb R^3$ with the same nonnegative initial density.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

362Global smoothness for relativistic Vlasov–MaxwellPartial differential equations
365Joint metric and connection recovery from one boundary patchPartial differential equations
366The planar Mumford–Shah regularity conjecture and local weak- L 4 gradient boundsPartial differential equations
367The critical dimension for the one-phase Bernoulli problemPartial differential equations
364Kinetic limits and fluctuations over the Boltzmann lifespanPartial differential equations

Browse Partial differential equations Open since the 1980s Lean-checked results