Uniqueness of renormalized solutions of the hard-sphere Boltzmann equation
From OpenAI Aftermath
Uniqueness of renormalized solutions of the hard-sphere Boltzmann equation concerns the large-data Cauchy problem for the Boltzmann equation of a dilute gas: whether a renormalized solution in the sense of DiPerna and Lions, with finite mass, energy and entropy, is determined by its initial datum. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), listed together as its result 363 and dated 23 September and 5 October 2026, claim that it is not: for the three-dimensional periodic hard-sphere equation each constructs one initial density with two distinct global solutions, the second within a class that also has exact local conservation of mass, momentum and kinetic energy. The collection includes a Lean formalization of the statement of the September manuscript. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- DiPerna and Lions established global existence and weak stability of renormalized solutions for data with finite mass, energy and entropy, together with an entropy-production inequality. Renormalization is needed because these bounds alone do not make the quadratic collision term locally integrable. In the periodic formulation of Levermore and Masmoudi, local mass is conserved, but the momentum and energy balances may carry nonnegative defects.
- Uniqueness holds under stronger control: in classes bounded by a multiple of a Maxwellian, by Kaniel and Shinbrot; for small periodic perturbations of a Maxwellian, by Ukai; and for large but bounded amplitudes with small relative entropy, by Duan, Huang, Wang and Yang. For the spatially homogeneous hard-sphere equation, Mischler and Wennberg proved uniqueness in the conservative class from finite mass and energy alone, while Wennberg's homogeneous nonuniqueness examples for hard potentials allow the energy to increase.
- Chen and Holmer, Chen, Shen and Zhang, and Chen, Guo, Shen and Zhang proved failure of uniform continuity of the solution map in weighted Sobolev spaces; these results compare nearby initial data. For the Krieger–Strain model, Gismondi, Golding and Novack constructed rough stationary solutions and conjectured nonuniqueness of renormalized solutions of the inhomogeneous Landau and Boltzmann equations.
The original results
- Claim, 23 September. Theorem 1.1 of Nonuniqueness for the periodic hard-sphere Boltzmann equation states that there is a nonnegative density on the three-dimensional torus times velocity space, with bounded velocity support and finite mass, kinetic energy and absolute entropy, for which the hard-sphere equation has two distinct global admissible solutions. Admissible means renormalized, weakly continuous in L1, with local conservation of mass, conservation of total momentum, the global energy inequality and the relative-entropy inequality with the full entropy dissipation; local conservation of momentum and energy is not required. On a common initial interval both solutions are strongly continuous in L1, and their collision gains and losses are integrable.
- Claim, 5 October. Theorem 1.1 of Nonuniqueness with local conservation for the hard-sphere Boltzmann equation states that there is a nonnegative datum with velocity support in a ball and finite mass, energy and absolute entropy that has two global entropy solutions with exact local conservation of mass, momentum and kinetic energy, including the initial traces, differing on a set of positive measure. Both are continuous in time with values in L1, and on every finite time interval their collision gains and losses are integrable against every polynomial velocity weight.
- Method, as described: the datum is made of cold jets, narrow velocity distributions near two opposite axial directions, on transverse annuli of geometrically decreasing radii, with the two velocity signs in finely alternating spatial stripes; the total mass, energy and entropy stay finite. One family of approximations starts without hot particles; in a second family, a vanishing hot seed is chosen so that the hot density attains a prescribed weighted bound. Dilation at the time of attainment gives a nonzero solution of a linear Boltzmann equation in a two-stream background, by velocity averaging and estimates on Carleman's gain kernels that prevent the attained size from vanishing in the limit; a branching argument shows that the dilated time horizon is finite; comparison with the first family then gives two distinct solutions. The October manuscript keeps this mechanism, which it reproduces with attribution, chooses the jet axis in a quadratic-irrational direction so that the jets do not meet their periodic copies during finite lifetimes, adds a nearly Maxwellian bath that gives a uniform collision frequency, and proves a global weighted estimate that yields the collision integrability needed for exact local conservation.
- Formalization, as described by the repository. The scope note states that the formalization proves nonuniqueness for the periodic hard-sphere equation by two distinct global renormalized solutions with the same nonnegative initial density, bounded velocity support and finite mass, energy and absolute entropy, which conserve local mass and total momentum, satisfy the global energy and entropy-dissipation inequalities, and are strongly continuous in L1 with integrable collision gains and losses on a common initial interval. It states that these are the conditions of the September result and that the later local-conservation refinements are outside it. The Comparator statement is
BoltzmannNonuniqueness.lean. - Sources (openai/math repository, commit
7ef5c0c): Nonuniqueness for the periodic hard-sphere Boltzmann equation, dated 23 September 2026; Nonuniqueness with local conservation for the hard-sphere Boltzmann equation, dated 5 October 2026.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | Boltzmann nonuniqueness and exact local conservation, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claims of the two manuscripts: nonunique rough solutions in an entropy class, and, in the later manuscript, nonuniqueness with exact local conservation of momentum and energy, which the article calls a substantive addition. It covers collisions and entropy, the two levels of nonuniqueness, why collision integrability gives local conservation, and the concentration, amplification and global continuation steps. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-07 | J. Evans, comment on his LinkedIn post about the release, with linked working notes | Remark | Describes the construction as highly bespoke but as joining two recognizable lines of PDE constructions: the instability line of Vishik and of Albritton, Brué and Colombo, and the concentration-and-gluing line around convex integration. It reads the October manuscript as repairing the construction until exact local conservation closes without destroying the instability. | LinkedIn comment; the author describes such notes as working genealogy notes, not priority claims, independent proof checks or reconstructions of the model's discovery process. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker-statement" against its summary. The Lean statement gives two renormalized solutions with local mass conservation, global momentum conservation and the global energy and entropy-dissipation inequalities, strongly continuous in L1 with integrable gains and losses only on a common initial interval; the exact local conservation of momentum and kinetic energy and the strong continuity for all times are not stated, as the scope note says. It lists the hand-built kinetic definitions of the collision integrals and the entropy dissipation among the definitions to check. | MathVet states that it does not claim any theorem false; its tables record no machine check for this challenge. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the BoltzmannNonuniqueness solution, in 1,378 s. |
Repository. |
| 2026-10-13 | M. Colbrook and contributors, AIM — Open Applied Problems (GitHub), problem 227 | Catalogue | The collection records its problem 227, uniqueness of entropy-admissible renormalized solutions of the periodic hard-sphere equation, as solved by the October manuscript, which it describes as a complete counterexample. It notes that the datum is rough, so that its problem 074 on smooth data is not resolved. | The status review is described as an AI statement-level comparison with the published manuscript, not an independent audit of the complete proof or a Lean kernel replay; it notes that the Lean scope covers the earlier periodic theorem. The collection is not affiliated with the American Institute of Mathematics. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews rank_415 and rank_365 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Both reviews report no gap. The review of the September manuscript records one minor note: in the separation argument, the branches of the nonzero-limit proposition with a positive scale ratio serve only the branching contradiction, which the paper does not say. It states that the cold-jet control and some kernel lemmas were taken on trust. The review of the October manuscript states that it read the construction, the global continuation, the compactness and local-conservation step and the separation in full, checked the Diophantine separation of the jet tubes and the barrier computations, and took the dilation, nonconcentration and branching sections adapted from the September manuscript on trust. The review of the September manuscript states that it checked the corresponding sections there in detail, which closes much of that dependency. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
| 2026-10-19 | AI Proved What?, episode 363 Same gas, two futures?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of two claims: a periodic starting density of a hard-sphere gas, with bounded velocities and finite mass, energy and entropy, has two different global solutions that conserve mass locally and momentum in total, with the energy only kept from growing; and a modified density has two different global solutions with exact local conservation of mass, momentum and energy and continuity in time for all time. The episode recalls that DiPerna and Lions proved global existence of renormalized solutions in 1989, that Silvestre wrote in 2022 that uniqueness in this class is unknown, and that Gismondi, Golding and Novack conjectured nonuniqueness in August 2026. It states that nonuniqueness for smooth data or for a whole class of data is not claimed, since the starting density has unbounded peaks at ever smaller scales, that the papers do not use convex integration, and that it found no competing claim. It also reports its own exact check of 3,000 collisions and a random-collision toy model. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as preprints: OpenAI, 78 + 65 pages, dated October 5 and September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the September paper’s theorem only, the headline local-conservation theorem has no Lean proof. The page states that both papers are unrefereed and unchanged since release, that the site did not run the Lean formalization of about 160,000 lines, and that it found no specialist comment and no reported error. |
Notes
- The background summarizes the manuscripts' own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
