Infinite enough?
An AI preprint claims to settle most of Kirchberg and Rørdam’s question on pure infiniteness, with Lean proofs
Covers result 303 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:09. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
In Hilbert’s hotel two copies fit inside one. In a C*-algebra, a positive element is properly infinite when two copies of it fit inside it, in the sense of Cuntz comparison; in matrices comparison is just rank comparison, so nothing nonzero there is properly infinite. For simple algebras there is one clean notion of pure infiniteness. For algebras with ideals, Kirchberg and Rørdam found three: weak, where for one fixed n, n copies of every positive element are properly infinite; ordinary, where every positive element is properly infinite; and strong, where any two positive elements can be pulled apart, each keeping its shape, approximately. Strong implies ordinary, and ordinary implies weak. In 2002 they asked whether the arrows reverse for all C*-algebras; Schafhauser, Tikuisis and White list it as Problem LXXII. Many special cases were known, including simple algebras, real rank zero and topological dimension zero.
Result 303 is one OpenAI paper, 52 pages, dated September 25, 2026, and made public October 6. It claims that ordinary pure infiniteness implies strong for every complex C*-algebra, and that for exact algebras weak implies ordinary, so all three notions agree. Combined with Kirchberg’s absorption theorem, every separable nuclear weakly purely infinite algebra absorbs the Cuntz algebra 𝒪∞, with no unit or simplicity assumed.
What it doesn’t claim
Whether weak implies ordinary for algebras that are not exact. The paper leaves that case outside its conclusions, and other recent surveys still call it open.
Where it stands
- Posted as a preprint
- OpenAI, 52 pages, dated September 25, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- Both main theorems; the corollary is proved too, but not as a posted challenge (docs)
Last checked October 19, 2026. The paper has not been revised. Both main theorems have Lean proofs, checked against posted challenge statements that look faithful to us, in an import closure of about 150,000 lines. Our scan finds no unproved steps; we did not build it. Two outside re-runs report that the Lean kernel accepts them. The corollary is also proved in the repository, but its statement is not one of the posted challenges. OSVerify has not reviewed it, and we found no expert comment.
How the proof goes
- Ordinary to strong. A transport lemma moves whole corners of the algebra along a single partial isometry. If two corners could not be pulled apart, finitely many freely chosen entries would be forced to equal values fixed in advance. Four entries, chosen using proper infiniteness, break that prescription, and repeating the step makes the cross term as small as you like.
- Weak to ordinary: halving. An element x with x² = 0 gives two orthogonal, equivalent halves inside a piece, and halving enough times produces n copies inside one piece. Exactness gives one error bound that works in every quotient at once, and that is what lets the paper find such an x across a whole slice of the algebra.
The numbers in the video
- Ours: in the strong test with the identity matrix taken twice, the best possible error in matrices is exactly 1/2; in the hotel it is 0, and a cross term pushed down the corridor shrinks from about 0.24 to 5 × 10⁻¹⁰.
- Ours: halving in 16 × 16 matrices gives ranks 8, 4, 2, 1 and stops; in the hotel it never ends.
Read the source
- Weak Pure Infiniteness and 𝒪∞ Absorption (PDF), 52 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 303.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
In Hilbert’s hotel, every guest in room k moves to room 2k, and a second hotel’s guests move to the odd rooms: two copies fit inside one. In a C*-algebra, a positive element is properly infinite when two copies of it fit inside it, in the sense of Cuntz comparison. Our computer checks the hotel, and checks that in matrices comparison is just rank comparison: three dimensions never fit into two, and two copies always need twice the rank, so nothing nonzero in a matrix algebra is properly infinite. For simple algebras there is one clean notion of pure infiniteness. For algebras with ideals, Kirchberg and Rørdam found three: weak, where for one fixed n, n copies of every positive element are properly infinite; ordinary, where every positive element is properly infinite; and strong, where any two positive elements can be pulled apart, each keeping its shape, approximately. Strong implies ordinary, and ordinary implies weak. In 2002 they asked whether the arrows reverse, for all C*-algebras. Schafhauser, Tikuisis and White list it as Problem LXXII. Many special cases were known, including simple algebras, real rank zero and topological dimension zero. Our computer runs the strong test on two positive elements: keep each one, and make the cross term small. With the identity matrix taken twice, the best possible error is exactly 1/2. In the hotel it is zero, and pushing a cross term down the corridor shrinks it from about a quarter to 5 × 10⁻¹⁰.
1:40The claim
Result 303 is one OpenAI paper, 52 pages, dated September 25 and made public October 6, 2026. It claims that ordinary pure infiniteness implies strong pure infiniteness for every complex C*-algebra, and that for exact algebras weak implies ordinary, so all three notions agree. Combined with Kirchberg’s absorption theorem, this gives the corollary: every separable nuclear weakly purely infinite algebra absorbs the Cuntz algebra 𝒪∞, with no unit or simplicity assumed. Not claimed: whether weak implies ordinary for algebras that are not exact. The paper leaves that case open.
2:24How the proof goes
For ordinary to strong, a transport lemma moves whole corners of the algebra along a single partial isometry. If two corners could not be pulled apart, finitely many freely chosen entries would be forced to equal values fixed in advance. Four entries, chosen using proper infiniteness, break that prescription, and repeating the step makes the cross term as small as you like. For weak to ordinary, the engine is halving: an element x with x² = 0 gives two orthogonal, equivalent halves inside a piece, and halving enough times produces n copies inside one piece. Our computer shows how halving runs out in finite algebras: in 16 × 16 matrices the ranks go 8, 4, 2, 1, and stop, while in the hotel halving never ends. Exactness gives one error bound that works in every quotient at once, and that is what lets the paper find such an x across a whole slice of the algebra.
3:24Where it stands
The paper is unrefereed and unchanged since release. Both main theorems have Lean proofs, checked against formal statements that look faithful to us, in an import closure of about 150,000 lines; our scan finds no unproved steps, but we did not build it. Two outside re-runs report that the Lean kernel accepts them. The repository also proves the corollary in Lean, but that statement is not one of the posted challenges. We found no expert comment. If it holds, for exact algebras weak, ordinary and strong pure infiniteness are the same, and for separable nuclear algebras each is the same as absorbing 𝒪∞.
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.