Robert's trace-cone question

Robert's trace-cone question asks whether the cone of extended lower-semicontinuous tracial weights of a separable nuclear C*-algebra determines the algebra after tensoring with the Razak–Jacelon algebra and the compact operators. A manuscript in OpenAI's public mathematics collection, dated 25 September 2026, claims a positive answer for every separable nuclear C*-algebra, with arbitrary ideal structure. A Lean formalization added to the collection later covers a supporting step on ideals, not the classification theorem.

Background

As recounted in the manuscript's introduction:
- The Razak–Jacelon algebra. Razak's classification of simple inductive limits of stably projectionless building blocks made the cone of traces, with its scale, an effective classification invariant. Jacelon's construction singled out the Razak–Jacelon algebra W, which is simple, nuclear, stably projectionless and has a unique trace up to scaling. Tensoring with W removes the K-theoretic part of the classification problem.
- The question. The question is due to Leonel Robert. It was recorded in Santiago's 2012 conference abstract and is Problem LXVIII in the survey of Schafhauser, Tikuisis and White, whose formulation keeps every extended trace, including the weights that take only the values zero and infinity. According to the manuscript, the survey's May 2026 discussion describes the known simple and traceless cases and the difficulty already presented by one proper nonzero ideal.
- Tools and earlier cases. Elliott, Robert and Santiago developed the topological cone of extended traces and its relation to the Cuntz semigroup, and Robert identified tensoring with W with realification of that semigroup. In the simple tracial case, work of Elliott and Niu and of Elliott, Gong, Lin and Niu classifies by scaled traces, with the nuclear-dimension theorem of Castillejos and Evington as a regularity bridge. The traceless case is explained by Rørdam's absorption criterion and Kirchberg's classification by ideal lattices, with a complete proof by Gabe. Lin and Ng classified certain essential extensions by W under a universal coefficient theorem assumption.

The original result

Claim, 25 September 2026. The main theorem of The trace cone classifies Razak–Jacelon stabilizations states that if separable nuclear complex C*-algebras A and B have isomorphic cones of extended traces, as topological cones, then A ⊗ W ⊗ K ≅ B ⊗ W ⊗ K, where K denotes the compact operators. The cone consists of all additive, positively homogeneous, lower-semicontinuous tracial maps from the positive elements to [0, ∞], with no density condition, and its topology is defined through cuts of positive elements. The manuscript also states that the isomorphism can be chosen to realize the given cone map, and that it answers the trace-cone question positively.
Scope, as stated: the algebras may be nonunital, may have both finite and infinite subquotients and may have an arbitrary primitive ideal space; the only assumptions are separability and nuclearity, with no universal coefficient theorem assumption. The conclusion concerns the stabilized algebras, not A and B themselves.
Method, as described: Robert's realification turns the cone into the Cuntz semigroup of the stabilization. Existence and uniqueness arguments then run in a sequence algebra, with errors controlled ideal by ideal through fixed positive controllers; stable-uniqueness methods of Dadarlat and Eilers and Gabe's ideal-related absorption remove the errors in norm, and an approximate intertwining produces the isomorphism. The weights that take only the values zero and infinity are exactly the additive idempotents of the cone and recover the ideal lattice.
Sources. Commit adc7f12 of the openai/math repository: The trace cone classifies Razak–Jacelon stabilizations.
Formalization. The release at commit adc7f12 has no Lean scope note for this family. A scope note first added on 8 October 2026, in its version at commit 7ef5c0c, states that the Lean development proves the supporting ideal-transport result: an equivalence of trace cones induces an order isomorphism of closed two-sided ideals that carries the finite and zero ideals of each trace to those of its image, and the zero-or-infinity weights are exactly the additive idempotents. It states that the isomorphism of stabilized algebras, the existence of the stabilization models, the uniqueness and the final intertwining are outside the formalization. Comparator statement: TraceIdealTransportSupport.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 31 October 2026)
2026-10-07	Trace cones and Razak–Jacelon stabilization, an article of the Latent Seminar blog at lowrank.github.io	Reading, exposition	Explains family 301: stabilization and tracial weights; the classification statement; how infinite values encode ideals; rank functions and Cuntz comparison; local errors that keep their norm; regularized traces; correction and uniqueness interfaces; from sequence models to an actual isomorphism.	Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs, and that it does not verify the full construction or its external classification and absorption inputs. Read on 31 October 2026.
2026-10-10	MathVet, a GitHub review of openai/math, tables at repository commit `c76f1e4` of 14 October 2026	Review, fidelity of the formal statements	Rates this family "supporting-only": the Lean challenge states only the cone and ideal layer, for arbitrary complex C*-algebras, and contains no tensor product, no W or K, no separability or nuclearity and no isomorphism of algebras, so the classification theorem is not stated. It lists the encoding of the cone topology as a convergence criterion as a definition to check, and records a sandboxed Comparator pass on 10 October 2026.	Review repository. Read on 31 October 2026.
2026-10-18	AI Proved What?, episode 301 The cone decides? Robert's trace-cone question, remade version of 23 October 2026	Reading, exposition	Video explainer of the 62-page preprint. It recalls that Robert's question was recorded by Santiago in 2012 and listed by Schafhauser, Tikuisis and White as Problem LXVIII, where even the case of one proper nonzero ideal was open, and illustrates with small examples how the infinite values of traces recover ideals. It states that the preprint does not claim that the algebras themselves are isomorphic, anything about tensoring with W without the compact operators, anything beyond separable nuclear algebras, or which cones can occur.	Episode status, last checked 30 October 2026: posted as a preprint, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, in part: about 1,100 lines formalize a supporting step, not the classification theorem; the site's scan found no unproved steps but it did not build the development, and it found no expert comment. The site states that it is made with Anthropic's Claude. Read on 31 October 2026.

Notes

The background summarizes the manuscript's own account of earlier work.
The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.