Bose–Einstein condensation in the dilute Bose gas

Bose–Einstein condensation in the dilute Bose gas concerns whether a macroscopic fraction of the particles of an interacting Bose gas occupies a single one-particle state in the thermodynamic limit, at fixed density and fixed interaction. Four manuscripts in OpenAI's public mathematics collection (github.com/openai/math) make claims on this question:

• condensation in every ground state of the dilute three-dimensional hard-sphere gas;
• a density-uniform condensate bound for soft repulsive interactions;
• condensation at positive temperature;
• the leading quantum depletion.

This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the hard-sphere ground-state manuscript's introduction:
  • Penrose and Onsager's density-matrix criterion identifies condensation by a macroscopic one-particle occupation.
  • For hard spheres, Lee, Huang and Yang predicted a depleted fraction of order (ρa³)^1/2.
  • The energy theory runs from Dyson and from Lieb and Yngvason to the sharp Lee–Huang–Yang bounds of Fournais and Solovej and of Basti, Brooks, Cenatiempo, Olgiati and Schlein. The manuscript notes that these energy asymptotics do not determine single-orbital occupation.
• Earlier condensation theorems treat different limits:
  • the trapped Gross–Pitaevskii limit (Lieb and Seiringer);
  • the homogeneous positive-temperature Gross–Pitaevskii limit (Deuchert and Seiringer);
  • joint dilute and increasing-volume limits (Fournais; Chong, Liang and Nam; Junge).
• The manuscript states that Solovej's 2025 survey identifies fixed-density ground-state condensation as a major open problem.

The original results

• Ground-state condensation for hard spheres (24 September 2026).
  • Setting: the hard-sphere Hamiltonian on the torus (ℝ/Lℤ)³, the Dirichlet form of −Σ_iΔ_i on configurations with all pair distances greater than a.
  • Theorem: there are absolute constants ε₀, c₀ > 0 such that, whenever ρa³ < ε₀, every sequence of normalized bosonic ground states has a constant-orbital fraction with lim inf at least c₀. This holds along every sequence with N, L → ∞ and N/L³ → ρ.
  • Corollary: the same bound holds for density operators supported on the ground spaces.
  • The manuscript proves a positive fraction. It does not estimate the optimal depletion.
• Method, as described in that manuscript. The modulus of a ground state is again a ground function. A lower bound for its constant-orbital occupation comes from a positive fraction of well-separated cell pairs.
  • Comparisons between neighboring cells come from local trajectory changes, built on an exact stationary killed-Brownian law.
  • Rather than multiplying costs along a route, the proof averages changes over random routes and bounds the second moment of the averaged likelihood. The remaining cost is controlled by mutual encounters of two routes. The manuscript cites path methods of Benjamini, Pemantle and Peres, and of Abbe, Massoulié, Montanari, Sly and Srivastava, and their adaptation by Garban and Spencer.
  • A separate phase estimate recovers the bound for complex ground states.
• Density-uniform bound for soft interactions (27 September 2026). For each fixed bounded measurable, nonnegative, radial, finite-range interaction that is not almost everywhere zero, the manuscript claims a positive lower bound on the constant-orbital condensate fraction. The bound is uniform over all sufficiently small densities and over temperatures between zero and the square of the density, in the thermodynamic limit.
• Positive temperature (5 October 2026). For each fixed exclusion distance and every sufficiently small fixed density, the manuscript claims a strictly positive temperature, independent of the volume, at which the exact canonical Gibbs state of the hard-sphere gas has a positive condensate fraction in the thermodynamic limit.
• Quantum depletion (5 October 2026). At zero temperature, with the thermodynamic limit taken before the dilute limit, the manuscript claims the scaled Bogoliubov momentum distribution of the depleted particles. The depletion fraction is (8/(3√π))(ρa³)^1/2 + o((ρa³)^1/2).
• Sources. Commit 1581d4c of the openai/math repository:
  • Ground-state condensation in the dilute hard-sphere gas;
  • A density-uniform condensate bound for dilute Bose gases;
  • Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas;
  • Quantum depletion and momentum distribution in the dilute hard-sphere Bose gas.
• Formalization, as described by the repository.
  • The scope note lean/docs/267.md is titled for positive-temperature condensation and exact quantum depletion. It states that the formalization proves ground-state condensation in the dilute hard-sphere gas, "without a positive-temperature assertion".
  • The Comparator challenge HardSphere.lean states condensation_with_mixed. Its quantifiers are as in the September theorem: pure ground vectors and density operators supported on the ground space, on the torus, along all thermodynamic sequences.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "weaker-statement" against its summary. The challenge states zero-temperature ground-state condensation with a non-sharp constant, while the positive-temperature and sharp-depletion headlines are not stated. Records a sandboxed Comparator pass for HardSphere.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list HardSphere, so the challenge was accepted by con-leche and by Lean's official kernel.	Development journal.
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 HardSphere solution (1,640 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-13	AIM problem 196, "Bose condensation at fixed dilute density" (MColbrook/AIM)	Catalogue (statement-level comparison)	Marks its problem SOLVED, citing the density-uniform manuscript. The problem asks about a fixed smooth nonnegative radial potential, the ground state on the torus, and the constant-orbital fraction at fixed small density. AIM describes this as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". It notes that the hard-sphere formalization does not cover smooth potentials. It cites Chong, Liang and Nam (arXiv:2510.20493) as identifying thermodynamic condensation as open.	Repository.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.