The cone decides?
An AI preprint claims the trace cone classifies Razak–Jacelon stabilizations, answering Robert’s question
Covers result 301 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
3:50. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A trace measures the size of positive elements. Here traces are defined on positive elements, lower semicontinuous, with values up to infinity, and the cone of all of them, with a suitable topology, is the trace cone. For the functions on three points, and for the sum of matrix blocks of sizes 1, 2 and 5, the cone is the same cube [0, ∞]³, and its 8 elements with τ + τ = τ, traces taking only 0 and ∞, match the 8 ideals exactly. The Razak–Jacelon algebra W is simple and nuclear, with exactly one trace up to scaling, no nonzero projections even in matrices over it, and no K-theory. Tensoring with W and the compact operators throws away everything except, it was hoped, the trace cone. That is Robert’s question, recorded by Santiago in 2012 and listed by Schafhauser, Tikuisis and White as Problem LXVIII; the simple and traceless cases were known, but even the case of one proper nonzero ideal was still open.
Result 301 is one OpenAI paper, 62 pages, dated September 25, 2026, and published October 6. It claims that if two separable nuclear C*-algebras have isomorphic trace cones, as topological cones, then their tensor products with W and the compacts are isomorphic, for any ideal structure, even with both finite and infinite subquotients, and with no UCT assumption.
What it doesn’t claim
That the algebras themselves are isomorphic, or anything about tensoring with W without the compacts; anything beyond separable nuclear algebras; or a description of which cones can occur.
Where it stands
- Posted as a preprint
- OpenAI, 62 pages, dated September 25, 2026
- Peer reviewed
- Not yet
- Formalized in Lean
- In part: a supporting step, not the classification (docs)
Last checked October 19, 2026. The paper has not been revised. In Lean, only a supporting step is formalized, in about 1,100 lines: the trace cone determines the ideal lattice, and each trace’s finite and zero ideals. The classification theorem itself is not formalized. Our scan finds no unproved steps; we did not build it. OSVerify has not reviewed it, and we found no expert comment.
How the proof goes
- From the cone to an isomorphism. The proof turns the cone into the Cuntz semigroup of the stabilization, by Robert’s realification, then runs existence and uniqueness inside a sequence algebra, measuring errors ideal by ideal, and borrows Gabe’s ideal-related absorption.
- How the cone remembers ideals. Scaling a trace toward 0 or ∞ lands on the traces of its finite and zero ideals. For the unitized compacts a whole half-line of traces has the compacts as its finite ideal; for the unitized stable O₂ only the single ideal trace does, so the cones differ.
The numbers in the video
- Ours: the traces n·δ1/n on C[0,1] give the function t the value 1 for every n, while their limit gives 0; the cut values 0.99, 0.9, 0, 0, 0 show why the cone’s topology is defined with cuts.
- Ours: in Razak’s building blocks a projection would need endpoint ranks (n − 1)k and nk, which agree only at 0, and the K-theory vanishes.
Read the source
- The Trace Cone Classifies Razak–Jacelon Stabilizations (PDF), 62 pages.
- Santiago’s 2012 preprint recording Robert’s conjecture (arXiv).
- Schafhauser, Tikuisis and White’s problem list (arXiv; Problem LXVIII).
- The Lean formalization notes.
- The collection’s catalog, where this is result 301.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
A trace measures the size of positive elements. Here traces are defined on positive elements, lower semicontinuous, with values up to infinity, and the cone of all of them, with a suitable topology, is the trace cone. Our computer shows why the infinite values matter: for the functions on three points, and for the sum of matrix blocks of sizes 1, 2 and 5, the cone is the same, [0, ∞]³, and its 8 elements with τ + τ = τ, traces taking only zero and infinity, match the 8 ideals exactly. The Razak–Jacelon algebra W is simple and nuclear, with exactly one trace up to scaling, no nonzero projections even in matrices over it, and no K-theory. Our computer checks its building blocks: a projection would need endpoint ranks (n − 1)k and nk, which agree only at zero, and the K-theory vanishes. Tensoring with W and with the compact operators throws away everything except, it was hoped, the trace cone. That is Robert’s question, recorded by Santiago in 2012 and listed by Schafhauser, Tikuisis and White as Problem LXVIII: for a separable nuclear C*-algebra, does the trace cone alone determine its tensor product with W and the compacts? The simple and traceless cases were known, but the problem list said that even the case of one proper nonzero ideal was still open.
1:31The claim
Result 301 is one OpenAI paper, 62 pages, dated September 25 and published October 6, 2026. It claims that if two separable nuclear C*-algebras have isomorphic trace cones, as topological cones, then their stabilizations by W and the compacts are isomorphic, for any ideal structure, even with both finite and infinite subquotients, and with no UCT assumption. Not claimed: that the algebras themselves are isomorphic, or anything about tensoring with W without the compacts; anything beyond separable nuclear algebras; or a description of which cones can occur.
2:14How the proof goes
The proof turns the cone into the Cuntz semigroup of the stabilization, by Robert’s realification, then runs existence and uniqueness inside a sequence algebra, measuring errors ideal by ideal, and borrows Gabe’s ideal-related absorption. The topology on the cone uses cuts. Our computer shows why: the traces n times the point mass at 1/n give the value 1 to the function t for every n, while their limit gives 0, a gap that only the cut test handles. In a one-ideal example the cone sees the difference. For the unitized compacts, a whole half-line of traces has the compacts as its finite ideal, while for the unitized stable O₂, only the single ideal trace does. Scaling a trace toward zero or infinity lands on the traces of its finite and zero ideals, which is how the cone remembers where each trace is finite and where it vanishes.
3:11Where it stands
The paper is unrefereed and unchanged since release. In Lean, only a supporting step is formalized, in about 1,100 lines: the trace cone determines the ideal lattice, and each trace’s finite and zero ideals. The classification theorem itself is not formalized. Our scan finds no unproved steps, but we did not build it, and we found no expert comment. If it holds, a separable nuclear C*-algebra, once tensored with W and the compacts, is determined up to isomorphism by its cone of traces, whatever its ideals.
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.