Classifies separable nuclear complex C∗-algebras after tensoring with the Razak–Jacelon algebra and the compact operators, using their full topological cones of extended lower-semicontinuous tracial weights. This answers Robert’s trace-cone question, including algebras with arbitrary ideal structure and both finite and infinite subquotients. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
The independent assessments find that the Lean statements express a supporting step or a different result. Read the assessments
The paper states
In The trace cone classifies Razak–Jacelon stabilizations, 25 September 2026
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
Let A and B be separable nuclear complex C^*-algebras. If T(A) and T(B) are isomorphic as topological cones, then
where \K=\K(\ell^2(\N)) and all tensor products are spatial.
Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.
Lean is a language for mathematical statements and proofs that a computer can verify. The Lean statement below is shown beside its possible paper counterpart, with the reason they were linked. The outside readers find that the release’s Lean states a supporting or different result, so the theorem it is paired with is shown under its own heading.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
TraceIdealTransportSupportThe paper states
In The trace cone classifies Razak–Jacelon stabilizations, 25 September 2026
Let A and B be separable nuclear complex C^*-algebras. If T(A) and T(B) are isomorphic as topological cones, then
where \K=\K(\ell^2(\N)) and all tensor products are spatial.
The words they share: algebras, complex, cones, nuclear, separable, spatial.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
TraceIdealTransportSupport.lean, the release lists it as a main result.
theorem idealOrderIso_finIdeal (τ : ExtendedTrace A) : F.idealOrderIso τ.finIdeal = (F.toEquiv τ).finIdeal := by sorryThis file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
The file states 16 more theorems: idealOrderIso_, closed_, zero_, star_, smul_, add_, mul_, isClosed_, mul_, mul_, lowerSemicontinuous_, weight_, finiteIdeal_, le_, idempotent_, closedIdealEquivOfAdditive_.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express a supporting result (their term: “supporting-only”).
Their note: The challenge states only the cone/ideal layer: for arbitrary complex C*-algebras A, B and a TraceConeEquiv F (an additive, scale-preserving bijection of extended-trace cones preserving canonical convergence), the induced order isomorphism of closed ideals sends finIdeal τ and zeroIdeal τ to finIdeal (F τ) and zeroIdeal (F τ), together with the 0/∞ ideal weights, additive idempotents and the order criterion I ≤ J ↔ τ_I + τ_J = τ_I. It contains no tensor product, no W or K, no separability/nuclearity and no *-isomorphism of algebras, so the classification (thm:main) is not stated; the content matches only the supporting Proposition 'Transport of ideals’ (st:ideals).
Definitions the group asks readers to compare with the paper: ExtendedTrace: standard extended lower-semicontinuous tracial weight on A₊ (τ(0)=0, additive, τ(rx)=rτ(x) only for r>0, τ(x*x)=τ(xx*), lsc); no density or semifiniteness assumption, matching the paper; CanonicalConvergence / PreservesCanonicalConvergence / TraceConeEquiv: the cone topology is encoded as convergence of arbitrary filters (limsup of cuts ≤ σ ≤ liminf) instead of a TopologicalSpace, so ‘homeomorphism’ becomes ‘bijection preserving this convergence in both directions’; matches the paper’s net criterion but is a nonstandard encoding; zeroIdeal: defined as finIdeal of the 0/∞-valued supportWeight (closure of {x | τ(x*x)=0}) rather than directly as the kernel ideal; nonstandard presentation, equivalent after unfolding; [PartialOrder A] [StarOrderedRing A]: the C*-order is supplied by extra instance arguments instead of Mathlib’s CStarAlgebra order; StarOrderedRing.le_iff forces the usual order (standard); ClosedIdeal.weight: Classical.choose from closed_ideal_weight_exists; only its forced values (0 on the ideal, ∞ off it) matter (standard); NonUnitalCStarAlgebra A: any complex C*-algebra, not nec. separable or nuclear; the supporting lemmas are more general than the paper’s setting, which is harmless for a supporting result
“supporting-only”, in their words: The challenge statements state a lemma or auxiliary result, not the headline.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
cert-machine finds that the Lean statements express a supporting result (their term: “SUPPORT-ONLY”).
The gap they name: The classification itself (spatial classification, stabilization models, norm uniqueness, intertwining).
“SUPPORT-ONLY”, in their words: The challenge statements state only supporting results.
Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
OpenAI’s own note on what its Lean covers
The paper classifies separable nuclear complex $C^*$-algebras after tensoring with the Razak–Jacelon algebra and the compact operators, using their cones of extended lower-semicontinuous traces. The linked formalization proves the ideal-transport part: a trace-cone equivalence induces an order isomorphism of closed two-sided ideals, carrying the ideals determined by finiteness and vanishing of each trace to those of its image.
For each closed ideal $I$, it also constructs the trace that is zero on positive elements of $I$ and infinite elsewhere. These traces are exactly the additive idempotents, meaning $\tau+\tau=\tau$, and their addition recovers ideal inclusion. Spatial classification, existence of the stabilization models, norm uniqueness, and final intertwining are outside this supporting comparison.
Transport of trace ideals and their additive-idempotent description TraceIdealTransportSupport
Unreviewed AI draft: states a supporting result. States the transport of ideals under trace-cone equivalences and the description of ideal traces as additive idempotents, one of the five supporting comparisons named in the Comparator README. The classification theorem itself is outside it.
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
TraceIdealTransportSupportThree reports, all at the release’s recorded version.
| Reported by | Their word | Their account | Date | Original report |
|---|---|---|---|---|
| cert-machine | “CERTIFIED” | Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution. | 10 October 2026 | Original report |
| MathVet | “comparator-sandboxed-pass” | Re-run through Comparator in a sandboxed virtual machine: accepted. | 10 October 2026 | Original report |
| Neal McBurnett, openai-math-lean-tooling | “accepted” | Re-run through Comparator with the nanoda kernel as well as Lean’s: accepted (the check took 147 s; peak memory 6.5 GiB). | 10 October 2026 | Original report |
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
No paper elsewhere in the release cites this family’s papers.
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Offer to write an explanationCompare the Lean statement with the paperSuggest a source attributionSuggest a change
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Solid publication, could lead to tenure”. The page says that nothing on it is verified.
Author not stated. Source
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Why this passage is shown
Theorem 1.1
In The trace cone classifies Razak–Jacelon stabilizations, 25 September 2026
Independent assessment
MathVet
14c7f91Independent assessment
Carlos Toledo’s cert-machine
9814e4cProof-verification report
cert-machine, TraceIdealTransportSupport
Proof-verification report
MathVet, TraceIdealTransportSupport
Proof-verification report
Neal McBurnett, openai-math-lean-tooling, TraceIdealTransportSupport
Lean statement
TraceIdealTransportSupport