View source for 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 ([https://github.com/openai/math 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''<sup>3</sup>)<sup>1/2</sup>.
** 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''ℤ)<sup>3</sup>, the Dirichlet form of −Σ<sub>''i''</sub>Δ<sub>''i''</sub> on configurations with all pair distances greater than ''a''.
** ''Theorem:'' there are absolute constants ''ε''<sub>0</sub>, ''c''<sub>0</sub> > 0 such that, whenever ''ρa''<sup>3</sup> < ''ε''<sub>0</sub>, every sequence of normalized bosonic ground states has a constant-orbital fraction with lim inf at least ''c''<sub>0</sub>. This holds along every sequence with ''N'', ''L'' → ∞ and ''N''/''L''<sup>3</sup> → ''ρ''.
** ''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''<sup>3</sup>)<sup>1/2</sup> + ''o''((''ρa''<sup>3</sup>)<sup>1/2</sup>).
* '''Sources.''' Commit <code>1581d4c</code> of the openai/math repository:
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026 ''Ground-state condensation in the dilute hard-sphere gas''];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026 ''A density-uniform condensate bound for dilute Bose gases''];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Bose-Einstein-condensation-at-positive-temperature-in-the-dilute-hard-sphere-gas-October-5-2026 ''Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas''];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Quantum-Depletion-and-Momentum-Distribution-in-the-Dilute-Hard-Sphere-Bose-Gas-October-5-2026 ''Quantum depletion and momentum distribution in the dilute hard-sphere Bose gas''].
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/267.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/HardSphere.lean HardSphere.lean] states <code>condensation_with_mixed</code>. 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 ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 16 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>HardSphere</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions does not list <code>HardSphere</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/3e3937cd5e4a4cacd451447c4ed8033eb0340521/corpus/openai-math/kernel-runs/38051470892/HardSphere.json cert-machine], openai/math lane K, run 38051470892 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>HardSphere</code> solution (1,640 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-13 || [https://github.com/MColbrook/AIM/blob/1b7c7fd251c1643bb41f0e3cef38704bcef410fd/problems/196-thermodynamic-bose-condensation.md 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 ([https://arxiv.org/abs/2510.20493 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.

[[Category:OpenAI results]]