# Positive-temperature Bose–Einstein condensation and exact quantum depletion > Proves condensation in every ground state of the dilute hard-sphere Bose gas; claims thermal and depletion laws. Canonical: https://closedform.nishachay.tech/e/openai-math-2026-267/ Last updated: 2026-10-14 **Proves condensation in every ground state of the dilute hard-sphere Bose gas; claims thermal and depletion laws.** **Trust:** Formal proof listed · **Papers:** 5 · **First paper:** September 24, 2026 · **Field:** Mathematical physics · **Entry:** 267 *Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error. Bose–Einstein condensation means a positive share of all particles sits in one single state. For interacting gases at fixed density, no one had proved it happens, even in the simplest model of hard balls. One paper shows a fixed positive share condenses in every ground state of a dilute hard-sphere gas, and Lean checks this. Four more papers claim condensation at small positive temperature and the exact share knocked out of the condensate. ## At a glance - **First step:** 1925 (Satyendra Nath Bose and Albert Einstein, condensation prediction for the ideal Bose gas) - **Significance:** Major. Condensation in an interacting gas at fixed density is a famous open problem; a 2025 survey calls it a major open problem. - **Trust:** Formal proof listed - **Field:** Mathematical physics (5 papers) ## The explanation Put N bosons, particles that may share a state, in a large box. Make them hard balls of diameter a: no two centres can come closer than a. The density ρ is particles per unit volume. The key number is the gas parameter ρa³, a rough measure of how crowded the gas is. Take ρa³ = 10⁻⁶, a very thin gas. Without interactions, at zero temperature, every particle would sit in the same flat, constant wave. Collisions knock some out of it. That missing share is called the depletion. Bose–Einstein condensation means a single one-particle state holds a macroscopic part of the system[1]. Penrose and Onsager gave the test: the occupation of one state must stay a fixed fraction of N[2]. Lee, Huang and Yang predicted a depleted fraction of order √(ρa³)[3]. For our gas that is of order 0.001, so about 99.9% should stay in the condensate. The energy of this gas has been worked out in detail. But those energy results do not settle single-state occupation, because the energy gap between states shrinks as the box grows[4]. A tiny gap means many states have almost the same energy. Particles could spread over them without costing much. Solovej's 2025 survey calls fixed-density ground-state condensation a major open problem[5]. The fifth paper settles the ground-state case. For a small enough fixed gas parameter, the constant wave holds a positive fraction of the particles as the box grows[6]. It holds for every ground state, and one fraction works for all small ρa³. It does not find the best fraction[7]. The other papers claim more. For hard spheres at zero temperature, the share outside the condensate is claimed to be (8/(3√π))√(ρa³), plus smaller terms[8]. The factor 8/(3√π) is about 1.5045. At ρa³ = 10⁻⁶ the depletion is about 0.0015, or 0.15%. The same law is claimed for bounded, repulsive, short-range interactions[9]. At positive temperature, one paper claims condensation persists up to a fixed temperature that does not depend on the box size[10]. For bounded repulsive interactions, another claims a condensate bound for all temperatures from zero up to ρ²[11]. How sure is this? Lean, a computer proof checker, proves the ground-state result. It covers every pure ground state and every mixture of them, with one constant for all small gas parameters. It does not cover positive temperature or the depletion law. Those rest on four long papers, and no specialist review of them has been published. **What it doesn't show.** This does not show condensation at every temperature below the critical one, or in dense gases such as liquid helium. ## 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 if it holds. Ground-state condensation for hard spheres has a Lean proof; the positive-temperature and exact depletion claims rest on unreviewed papers. ## Words used - **Boson:** A kind of particle that can share the same quantum state with others of its kind. - **Bose–Einstein condensation:** A fixed positive share of all particles sitting in one single quantum state. - **Hard-sphere gas:** A model where particles are hard balls of diameter a that cannot overlap and otherwise do not interact. - **Gas parameter ρa³:** Density times the cube of the ball size; small values mean a dilute gas. - **Thermodynamic limit:** Letting the number of particles and the box volume grow together at fixed density. - **Depletion:** The share of particles outside the condensate state. - **Ground state:** The lowest-energy state of the whole system, at zero temperature. ## The original papers (5) - [Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas](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) - October 5, 2026 - [Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas](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) - October 5, 2026 - [Quantum Depletion for Fixed Bounded Repulsive Potentials](https://github.com/openai/math/blob/main/preprints/Quantum-Depletion-for-Fixed-Bounded-Repulsive-Potentials-October-5-2026/fixed-repulsion-quantum-depletion.pdf) - October 5, 2026 - [A density-uniform condensate bound for dilute Bose gases](https://github.com/openai/math/blob/main/preprints/A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026/paper.pdf) - September 27, 2026 - [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf) - September 24, 2026 - [Lean notes](https://github.com/openai/math/blob/main/lean/docs/267.md) ## Quoted lines from the paper (11) [1] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > Bose--Einstein condensation means that a single one-particle state carries a macroscopic part of a many-particle system. [2] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > For an interacting gas, the density-matrix criterion of Penrose and Onsager identifies condensation through a macroscopic one-particle occupation. [3] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > For hard spheres, Lee, Huang and Yang's pseudopotential calculation predicts a depleted fraction of order $\sqrt{\rho a^3}$. [4] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > These energy asymptotics do not determine single-orbital occupation as the one-particle spectral gap vanishes in large volume. [5] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > Solovej's 2025 survey identifies fixed-density ground-state condensation as a major open problem. [6] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > At every sufficiently small fixed gas parameter, the constant orbital contains a positive fraction of the particles in the thermodynamic limit. [7] From [Ground-state condensation in the dilute hard-sphere gas](https://github.com/openai/math/blob/main/preprints/Ground-state-condensation-in-the-dilute-hard-sphere-gas-September-24-2026/paper.pdf): > We prove a positive fraction; we do not estimate the optimal depletion or show that the fraction tends to one as $\rho a^3$ tends to zero. [8] From [Quantum Depletion and Momentum Distribution in the Dilute Hard-Sphere Bose Gas](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): > 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 $\rho$ and hard-sphere exclusion distance $a$. [9] From [Quantum Depletion for Fixed Bounded Repulsive Potentials](https://github.com/openai/math/blob/main/preprints/Quantum-Depletion-for-Fixed-Bounded-Repulsive-Potentials-October-5-2026/fixed-repulsion-quantum-depletion.pdf): > 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$. [10] From [Bose–Einstein condensation at positive temperature in the dilute hard-sphere gas](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): > 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. [11] From [A density-uniform condensate bound for dilute Bose gases](https://github.com/openai/math/blob/main/preprints/A-density-uniform-condensate-bound-for-dilute-Bose-gases-September-27-2026/paper.pdf): > 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. ## Other sources - [openai/math, Lean scope note for family 267](https://github.com/openai/math/blob/main/lean/docs/267.md): “The formalization proves ground-state Bose–Einstein condensation in the dilute hard-sphere gas.” - [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model” ## Related - [Bloch's law, its lattice correction, and the spherical magnetization law](https://closedform.nishachay.tech/e/openai-math-2026-271/) - Mathematical physics - [Parity is not in QAC 0](https://closedform.nishachay.tech/e/openai-math-2026-274/) - Mathematical physics - [Classical capacity of generalized amplitude damping](https://closedform.nishachay.tech/e/openai-math-2026-276/) - Mathematical physics - [Exact quantum factoring over a fixed finite gate set](https://closedform.nishachay.tech/e/openai-math-2026-279/) - Mathematical physics - [Polynomial-time unitary synthesis from a Boolean oracle](https://closedform.nishachay.tech/e/openai-math-2026-283/) - Mathematical physics - [Mathematical physics](https://closedform.nishachay.tech/science/mathematics/mathematical-physics/) - Field · 25 results - [Quantum theory](https://closedform.nishachay.tech/topic/quantum/) - Topic · 9 results - [Open since before 1940](https://closedform.nishachay.tech/open-since/before-1940/) - Era · 16 results - [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results - [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20267%5D%20)