AI Proved What?

Episode 267, October 2026

A condensate, proved at last?

Five AI preprints claim Bose–Einstein condensation for the interacting hard-sphere gas, and the quantum depletion law

Covers result 267 in OpenAI’s catalog: all 5 papers. See its connections to other results and the work it cites.

4:22. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The question
  2. 1:16The claims
  3. 2:49How the proofs go
  4. 3:30Where it stands

The claim, in plain words

Cool a gas of bosons enough and a macroscopic fraction of the particles piles into a single quantum state. Bose–Einstein condensation was predicted in 1925 and seen in rubidium in 1995. For an ideal gas with no interactions, Einstein computed it exactly: below a critical temperature, the condensed fraction is 1 − (T/Tc)3/2. Condensation means long-range order: the one-particle density matrix does not decay to zero at large distances.

For real, interacting particles in continuous space at fixed density, this had never been proved. The only interacting case known in the thermodynamic limit was hard-core bosons on a lattice at half filling. A 2025 survey by Solovej called ground-state condensation one of the major open problems, and a 2005 book by Lieb, Seiringer, Solovej and Yngvason wrote that the problem remained open after more than 75 years.

Result 267 is five OpenAI preprints, 279 pages, dated September 24 to October 5, 2026. The headline paper claims condensation for the exact canonical Gibbs state of the three-dimensional hard-sphere gas. For each sphere size and small enough density there is a fixed positive temperature, independent of the volume, at which a positive fraction of particles occupies the lowest state in the thermodynamic limit. Companions claim condensation for every ground state of dilute hard spheres, and for bounded repulsive potentials at small temperatures. Two more claim the quantum depletion law at zero temperature: to leading order, the fraction of particles kicked out of the condensate by interactions is 8/(3√π) times √(ρa³), taking the infinite volume first.

What it doesn’t claim

The temperature is tiny. Its formula is explicit up to constants the paper never computes; at ρa³ = 10⁻⁶, if that is dilute enough, it is below 10⁻⁷ of the ideal critical temperature (our arithmetic). Not claimed: condensation all the way up to the transition, the shift of the critical temperature, two dimensions, attractive or helium-like interactions, or depletion at positive temperature.

Where it stands

Posted as preprints
OpenAI, five papers, 279 pages, dated September 24 to October 5, 2026
Peer reviewed
Not yet
Formalized in Lean
In part: the ground-state theorem (docs)

Last checked October 19, 2026. The preprints have not been revised. Lean formalizes only the ground-state theorem, about 72,000 lines with no unproved steps, which we did not build, and explicitly not the positive-temperature result. OSVerify has not reviewed them. One depletion paper relies on a recent preprint by Basti and coauthors that we found no sign has been refereed. We found no comment from specialists such as Seiringer, Solovej or Schlein. Commenting on the whole release, a mathematical physicist wrote that several central problems of their subfield were claimed as solved, and that a first look at the preprints was disappointing: “unreadable”.

How the proofs go

  1. Cells and random routes. The proofs divide space into cells holding many particles. They show that a particle here and a particle far away see the same surroundings, by shifting a chain of particles one cell each along random lattice routes that rarely meet. This forces occupation of the constant orbital.
  2. Hard core and depletion. The hard core is handled by local energy bounds and careful particle insertions. The depletion law comes from a Bogoliubov analysis inside large boxes, with the path comparison controlling differences between boxes.

The numbers in the video

  • Ours: in a finite box of ideal bosons at half the critical temperature, the correlation levels off at 0.669, matching that box’s own condensed fraction.
  • Ours: the depletion constant 8/(3√π) = 1.5045, reproduced numerically.

Read the source

The 5 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The question

Cool a gas of bosons enough and a macroscopic fraction of the particles piles into a single quantum state: Bose–Einstein condensation, predicted in 1925 and seen in rubidium in 1995. For an ideal gas with no interactions, Einstein computed it exactly: below a critical temperature, the condensed fraction is one minus the temperature ratio to the 3/2. Condensation means long-range order: the one-particle density matrix does not decay to zero at large distances. Our computer shows it in a finite box of ideal bosons at half the critical temperature: the correlation levels off at 0.669, matching that box’s own condensed fraction. Above the critical temperature it falls to zero. For real, interacting particles in continuous space at fixed density, this had never been proved. The only interacting case known in the thermodynamic limit was hard-core bosons on a lattice at half filling. A 2025 survey by Solovej called ground-state condensation one of the major open problems, and a 2005 book by Lieb, Seiringer, Solovej and Yngvason wrote that the problem remained open after more than 75 years.

1:16The claims

Result 267 is five OpenAI preprints, 279 pages, dated September 24 to October 5, 2026. The headline paper claims condensation for the exact canonical Gibbs state of the three-dimensional hard-sphere gas: for each sphere size and small enough density there is a fixed positive temperature, independent of the volume, at which a positive fraction of particles occupies the lowest state in the thermodynamic limit. Companions claim condensation for every ground state of dilute hard spheres, and for bounded repulsive potentials at small temperatures. Two more claim the quantum depletion law at zero temperature: the fraction of particles kicked out of the condensate by interactions is, to leading order, 8/(3√π) times the square root of the density times the scattering length cubed, taking the infinite volume first. Our computer reproduces that constant, 1.5045. The temperature is tiny. Its formula is explicit up to constants the paper never computes; with the smallest allowed value, at density times scattering length cubed of 10⁻⁶, and if that is dilute enough, it is less than 10⁻⁷ of the ideal critical temperature. Not claimed: condensation all the way up to the transition, the shift of the critical temperature, two dimensions, attractive or helium-like interactions, or depletion at positive temperature.

2:49How the proofs go

The proofs divide space into cells holding many particles, and show that a particle here and a particle far away see the same surroundings, by shifting a chain of particles one cell each along random lattice routes that rarely meet; this forces occupation of the constant orbital. The hard core is handled by local energy bounds and careful particle insertions, and the depletion law by a Bogoliubov analysis inside large boxes, with the path comparison controlling differences between boxes. One depletion paper relies on a recent preprint by Basti and coauthors that we found no sign has been refereed.

3:30Where it stands

The preprints are unrefereed and unchanged since release. Lean formalizes only the ground-state theorem, about 72,000 lines with no unproved steps, which we did not build, and explicitly not the positive-temperature result. OSVerify has not reviewed them. We found no comment from specialists such as Seiringer, Solovej or Schlein; commenting on the whole release, a mathematical physicist wrote that several central problems of their subfield were claimed as solved, and that a first look at the preprints was disappointing: unreadable. If they hold, Bose–Einstein condensation is at last a theorem for a genuinely interacting gas in continuous space at fixed density, at positive temperature, though far below where it actually happens.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.