Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stability

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Proves equivariant Jiang–Su stability for every countable discrete amenable group action on a simple separable unital infinite-dimensional nuclear stably finite Jiang–Su-stable C∗-algebra, resolving this case of Szabó’s conjecture without restrictions on trace dynamics. The family also proves the unital Toms–Winter conjecture, equating strict comparison, finite nuclear dimension and Jiang–Su stability in the simple separable unital infinite-dimensional nuclear setting. (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

Theorem 1.1

In Equivariant Jiang–Su Stability for Amenable Actions in the Unital Stably Finite Case, 5 October 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.

13 other possible matches are listed below the card, among them Theorem 1.1 (Real rank zero and uniform property \Gamma) in Tracial projection methods and uniform property Gamma and Theorem 1.4 (The direct unital comparison route) in Tracial projection methods and uniform property Gamma.

Let A be a simple, separable, unital, infinite-dimensional, nuclear, stably finite complex \mathrm C^*-algebra satisfying A\cong A\otimes\Zalg. Let G be a countable discrete amenable group and let \alpha:G\to\Aut(A) be any action. Put

B=A\otimes\Zalg,\qquad \beta_g=\alpha_g\otimes\operatorname{id}_{\Zalg}.

There are a unital *-isomorphism \Phi:A\to B and unitaries u_g\in B, g\in G, such that

\begin{aligned}u_e&=1,& u_{gh}&=u_g\beta_g(u_h),\\ \Phi(\alpha_g(a))&=u_g\beta_g(\Phi(a))u_g^* &&(g\in G,\ a\in A).\end{aligned}

No Lean statement in the release is paired with this theorem.

13 more possible matches

  • Theorem 1.1 (Real rank zero and uniform property \Gamma) in Tracial projection methods and uniform property Gamma.
  • Theorem 1.4 (The direct unital comparison route) in Tracial projection methods and uniform property Gamma.
  • Theorem 1.1 (Simple comparison and absorption) in Cuntz comparison and Jiang–Su absorption.
  • Theorem 1.5 (The direct stably projectionless route) in Tracial projection methods and uniform property Gamma.
  • Theorem 1.2 (Absorption from condition (C)) in Cuntz comparison and Jiang–Su absorption.
  • Corollary 1.4 (An abstract Cuntz-semigroup criterion) in Cuntz comparison and Jiang–Su absorption.
  • Corollary 1.3 (The canonical Cuntz-semigroup map) in Cuntz comparison and Jiang–Su absorption.
  • Theorem 1.3 (Sharp bound after Jiang–Su absorption) in Nuclear dimension and Jiang–Su stability without elementary subquotients.
  • Theorem 1.1 (Nonsimple nuclear regularity) in Nuclear dimension and Jiang–Su stability without elementary subquotients.
  • Theorem 1.4 (Full signs in a finite maximal tensor power) in Nuclear dimension and Jiang–Su stability without elementary subquotients.
  • Theorem 1.3 (Finite-set central splitting) in Tracial projection methods and uniform property Gamma.
  • Corollary 1.2 (Traces on the completion) in Tracial projection methods and uniform property Gamma.
  • Corollary 1.2 (Regularity and Cuntz-semigroup criteria) in Nuclear dimension and Jiang–Su stability without elementary subquotients.
Reported proof verification
One Lean statement in the release; three independent groups report that Comparator accepted runs for this file at the version shown here.
Papers and explanations
Four current papers, each readable here as a page beside its PDF.

Papers

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.

Equivariant Jiang–Su Stability for Amenable Actions in the Unital Stably Finite Case

5 October 2026, current edition.

Read it herePDF

Every action of a countable discrete amenable group on a simple, separable, unital, infinite-dimensional, nuclear, stably finite complex C∗-algebra that is already Jiang–Su stable absorbs the trivial action on the Jiang–Su algebra up to cocycle conjugacy. No restriction is imposed on the action on the tracial-state simplex. This proves the unital, stably finite case of Szabó’s Conjecture A on automatic equivariant Jiang–Su stability.

Cuntz comparison and Jiang–Su absorption

Undated, current edition.

Read it herePDF

We prove that strict comparison in the extended-functional sense implies Jiang–Su absorption for separable simple nuclear non-elementary C∗-algebras. This resolves the corresponding implication of the Toms–Winter regularity problem, including nonunital algebras and allowing unbounded traces. More generally, every separable nuclear C∗-algebra whose Cuntz semigroup is almost unperforated and fully almost divisible absorbs the Jiang–Su algebra.

Nuclear dimension and Jiang–Su stability without elementary subquotients

Undated, current edition.

Read it herePDF

For separable nuclear C∗-algebras with no nonzero elementary ideal subquotients, finite nuclear dimension is equivalent to Jiang–Su stability. More generally, \(\dim_{\mathrm{nuc}}(A_0\otimes\mathcal Z)\le1\) for every separable nuclear A0. This proves Robert and Tikuisis’s Conjecture (C1) and the nuclear-dimension equivalence in the nonsimple Toms–Winter regularity question.

Tracial projection methods and uniform property Gamma

Undated, current edition.

Read it herePDF

For a simple, separable, unital, infinite-dimensional, nuclear, stably finite C∗-algebra with traces, real rank zero of the uniform tracial ultrapower of its uniform tracial completion implies uniform property Γ. This answers Problem XXI of Schafhauser, Tikuisis and White affirmatively. Independently, strict comparison implies Jiang–Su absorption for simple, separable, unital, infinite-dimensional nuclear algebras, resolving the unital Toms–Winter conjecture. Under comparison tested on traces of finite target rank, we also obtain uniform property Γ and absorption for simple, separable, nuclear, stably projectionless algebras whose densely finite traces are all bounded and have a nonempty compact normalized base.

One Lean statement in this family

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.

UniformGamma

The paper states

Theorem 1.1 (Real rank zero and uniform property \Gamma)

In Tracial projection methods and uniform property Gamma

Let A be a unital, separable, simple, infinite-dimensional, nuclear, stably finite C^*-algebra with T(A)\ne\varnothing, and let B=\overline A^{T(A)}. Fix any free ultrafilter \omega on \N. If B^\omega has real rank zero in its quotient C^*-norm, then there is a projection p\in B^\omega\cap B' such that

\lambda(px)=\tfrac12\lambda(x) \qquad(x\in B,\ \lambda\in\Lambda_\omega).

In particular, A has uniform property \Gamma.

The words they share: quotient, stably, ultrafilter, real, 1/2, rank, property, norm, gamma, simple, uniform, dimensional, projection, zero, finite, nuclear, separable, algebra, tracial, free, infinite, unital.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Uniform property $\Gamma$ from tracial real rank zero

UniformGamma.lean, the release lists it as a main result.

theorem CurrentMain.main : MainClaim.{uNuclear} := by  sorry

This 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.

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

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

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 single challenge is CurrentMain.main : MainClaim, i.e. Statement (for a simple separable nuclear stably finite infinite-dimensional C*-algebra with tracial states and a free ultrafilter U, if the uniform tracial ultrapower of the uniform tracial completion has real rank zero then UniformPropertyGammaAt A U), preceded by existential witnesses for the hand-built NormConstruction/NullConstruction/CauchyConstruction/LimitConstruction/TraceConstruction classes. This is a supporting technical implication (docs: ‘real rank zero... implies uniform property Γ’). The summary’s headline results, equivariant Jiang-Su stability for every countable discrete amenable group action and the unital Toms-Winter conjecture (strict comparison ⇔ finite nuclear dimension ⇔ Jiang-Su stability), are not stated.

Definitions the group asks readers to compare with the paper: The uniform tracial completion and ultrapowers are hand-built quotients: UniformTracialCompletion := (familyCauchyNullIdeal τ).Quotient, FamilyUltrapower := (familyNullIdeal τ U).Quotient, with class NormConstruction : Prop/NullConstruction/CauchyConstruction/LimitConstruction/TraceConstruction and MainClaim := ∃ h0 : NormConstruction,... ∃ h4 : TraceConstruction, Statement, i.e. the C*-algebra structure is posited as existentially provable classes inside the claim; IsNuclear and RealRankZero are also local definitions.

“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.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a different result (their term: “DIFFERENT”).

The gap they name: The only challenge (UniformGamma) states a different theorem from the 'Tracial projection methods’ manuscript: real rank zero of the uniform tracial ultrapower of the uniform tracial completion implies uniform property Γ (Schafhauser–Tikuisis–White Problem XXI). Neither headline clause is stated, and the stated theorem is neither implied by nor implies them.

“DIFFERENT”, in their words: The challenge statements state a different theorem from the headline.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The formalization proves that real rank zero of the uniform tracial ultrapower of the uniform tracial completion implies uniform property $\Gamma$ for a simple separable unital infinite-dimensional nuclear stably finite $C^*$-algebra with traces. The conclusion holds at every specified free ultrafilter under the corresponding real-rank-zero hypothesis.

The linked comparison results also prove Jiang–Su absorption and uniform property $\Gamma$ for simple separable unital infinite-dimensional nuclear algebras with strict comparison, and for the stated stably projectionless nuclear algebras with bounded densely finite traces, a nonempty compact normalized trace base, and the prescribed finite-target-rank comparison condition.

AI-drafted comparisons, with no recorded human review

  • Uniform property $\Gamma$ from tracial real rank zero UniformGamma

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem (tracial real rank zero implies uniform property Γ) and the paper’s comparison theorems giving Jiang–Su absorption under strict comparison and in the stated stably projectionless case.

Who ran the proof-verification program?

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.

Uniform property $\Gamma$ from tracial real rank zero UniformGamma

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal 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 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 544 s; peak memory 6.5 GiB).11 October 2026Original report

What these papers cite in the release, and what cites them

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.

Within this family

Explain a result, compare statements or propose a correction

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

What people have said

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 “Major math journal”. The page says that nothing on it is verified.

    Author not stated. Source

  • Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source

    The headline claims equivariant Jiang-Su stability and the unital Toms-Winter conjecture, but only a real-rank-zero implication for uniform property Gamma is formalised.

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 291 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 291 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form