Positive-temperature Bose–Einstein condensation and exact quantum depletion

5 papersLean

Proves Bose–Einstein condensation for the exact canonical Gibbs state of the three-dimensional hard-sphere gas: each fixed exclusion distance and sufficiently small fixed density admit a strictly positive temperature, independent of volume, with positive condensate fraction in the thermodynamic limit. At zero temperature, proves the Bogoliubov leading quantum-depletion law for hard spheres and fixed bounded nonnegative radial finite-range potentials of positive scattering length, taking the thermodynamic limit before the dilute limit.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 5

Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas

OpenAI · October 5, 2026

We prove Bose–Einstein condensation at positive temperature in the three-dimensional dilute hard-sphere gas. For each fixed exclusion distance and every sufficiently small fixed density, there is a strictly positive temperature, independent of the volume, at which the exact canonical Gibbs state has a positive condensate fraction in the thermodynamic limit. The condensate occupies the constant orbital.

Read PDF Download Source

Cite

@misc{OAI:Bose-Einstein-condensation-at-positive-temperature-in-the-dilute-hard-sphere-gas-October-5-2026,
  author = {{OpenAI}},
  title = {{Bose--Einstein condensation at positive temperature in the dilute hard-sphere gas}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Bose-Einstein-condensation-at-positive-temperature-in-the-dilute-hard-sphere-gas-October-5-2026/positive-temperature-hard-spheres.pdf}{OAI:Bose-Einstein-condensation-at-positive-temperature-in-the-dilute-hard-sphere-gas-October-5-2026}},
  year = {2026}
}

Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas

OpenAI · October 5, 2026

We prove the full scaled Bogoliubov momentum distribution for the depleted particles in the three-dimensional hard-sphere Bose gas at zero temperature. The thermodynamic limit is taken at each fixed density before the dilute limit, uniformly over all pure and mixed ground states. All thermodynamic accumulation values have the same dilute asymptotic: the limiting nonzero-momentum occupation measure has total mass \(8/(3\sqrt\pi)\), giving the depletion fraction \(\frac{8}{3\sqrt\pi}\sqrt{\rho a^3}+o(\sqrt{\rho a^3})\) for density ρ and hard-sphere exclusion distance a.

Read PDF Download Source

Cite

@misc{OAI:Quantum-Depletion-and-Momentum-Distribution-in-the-Dilute-Hard-Sphere-Bose-Gas-October-5-2026,
  author = {{OpenAI}},
  title = {{Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Quantum-Depletion-and-Momentum-Distribution-in-the-Dilute-Hard-Sphere-Bose-Gas-October-5-2026/Quantum-Depletion-in-the-Dilute-Hard-Sphere-Bose-Gas.pdf}{OAI:Quantum-Depletion-and-Momentum-Distribution-in-the-Dilute-Hard-Sphere-Bose-Gas-October-5-2026}},
  year = {2026}
}

Quantum Depletion for Fixed Bounded Repulsive Potentials

OpenAI · October 5, 2026

We prove the Bogoliubov quantum-depletion asymptotic for the ground state of a three-dimensional Bose gas with a fixed bounded, nonnegative, radial interaction of finite range and positive scattering length a. The thermodynamic limit is taken at each fixed density ρ before the dilute limit. Every thermodynamic accumulation value of the fraction outside the constant mode is \(\frac{8}{3\sqrt\pi}\sqrt{\rho a^3}+o(\sqrt{\rho a^3})\) as \(\rho\downarrow0\). The assertion is uniform over ground-state density matrices and does not require the occupation to have a unique thermodynamic limit.

Read PDF Download Source

Cite

@misc{OAI:Quantum-Depletion-for-Fixed-Bounded-Repulsive-Potentials-October-5-2026,
  author = {{OpenAI}},
  title = {{Quantum Depletion for Fixed Bounded Repulsive Potentials}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Quantum-Depletion-for-Fixed-Bounded-Repulsive-Potentials-October-5-2026/fixed-repulsion-quantum-depletion.pdf}{OAI:Quantum-Depletion-for-Fixed-Bounded-Repulsive-Potentials-October-5-2026}},
  year = {2026}
}

A density-uniform condensate bound for dilute Bose gases

OpenAI · September 27, 2026

For each fixed bounded measurable, nonnegative, radial interaction of finite range in three dimensions that is not zero almost everywhere, we prove a positive lower bound on the constant-orbital condensate fraction that is uniform over all sufficiently small densities and all temperatures between zero and the square of the density. The interaction and density remain fixed in the thermodynamic limit.

Read PDF Download Source

Cite

@misc{OAI:A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026,
  author = {{OpenAI}},
  title = {{A density-uniform condensate bound for dilute Bose gases}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026/paper.pdf}{OAI:A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026}},
  year = {2026}
}

Ground-state condensation in the dilute hard-sphere gas

OpenAI · September 24, 2026

We prove Bose–Einstein condensation in every ground state of a dilute three-dimensional hard-sphere Bose gas. At every sufficiently small fixed gas parameter, the constant orbital contains a positive fraction of the particles in the thermodynamic limit. The fraction can be chosen independently of the gas parameter, and the conclusion holds for arbitrary complex ground states.

Read PDF Download Source

Cite

@misc{OAI:Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026,
  author = {{OpenAI}},
  title = {{Ground-state condensation in the dilute hard-sphere gas}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf}{OAI:Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Ground-state condensation in the dilute hard-sphere gas

Scope

The formalization proves ground-state Bose–Einstein condensation in the dilute hard-sphere gas. There are absolute constants \(\varepsilon_0,c_0>0\) such that, whenever the density \(\rho\) and hard-sphere radius \(a\) satisfy \(\rho a^3<\varepsilon_0\), the condensate occupation fraction has limit inferior at least \(c_0\) along every thermodynamic sequence with \(N/L^3\to\rho\).

The bound covers every pure ground state, every mixed state supported on the ground space, and the normalized ground-space projection. It is uniform in the gas parameter within this range and concerns ground states, without a positive-temperature assertion.

Comparator links

Result	Comparator statement
Uniform ground-state condensation in the dilute hard-sphere gas	HardSphere.lean

Scope note on GitHub →