The Kirchberg–Rørdam character criterion for Jiang–Su stability
From OpenAI Aftermath
The Kirchberg–Rørdam character criterion for Jiang–Su stability concerns the question of Kirchberg and Rørdam whether a unital separable C*-algebra absorbs the Jiang–Su algebra exactly when its norm central-sequence algebra has no characters, that is, no nonzero homomorphisms to the complex numbers. One direction is elementary. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the criterion for every nonzero unital separable complex C*-algebra and every free ultrafilter, together with Jiang–Su stability of infinite tensor powers, with a Lean formalization of the criterion. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Toms and Winter developed the theory of strongly self-absorbing algebras, which recognizes tensorial absorption through central copies of the absorbed algebra. Kirchberg and Rørdam proved that a unital separable algebra is Jiang–Su stable exactly when its norm central-sequence algebra contains, with the same unit, a separable subhomogeneous subalgebra without characters, and asked whether the absence of characters on the whole central-sequence algebra already suffices.
- Kirchberg and Rørdam related the question to tensor powers of algebras without characters. Dadarlat and Toms showed that the infinite minimal tensor power of a unital separable algebra is Jiang–Su stable whenever it contains a same-unit subhomogeneous subalgebra without characters. The character question also appears as a problem in the recent collection of Schafhauser, Tikuisis and White.
The original result
- Claim. Theorem 1.1 of The Kirchberg–Rørdam character criterion states that for every nonzero unital separable complex C*-algebra A and every free ultrafilter, the norm central-sequence algebra of A has no characters if and only if A is isomorphic to its minimal tensor product with the Jiang–Su algebra. No nuclearity, simplicity, trace, dimension or comparison hypothesis is imposed. A corollary states that the infinite minimal tensor power of every nonzero unital separable C*-algebra without characters is Jiang–Su stable and contains a unital copy of the Jiang–Su algebra.
- Method, as described: the main ingredient is a finite construction: every nonzero unital C*-algebra without characters receives a unital homomorphism from the dimension-drop algebra I(2,3) in some finite maximal tensor power of itself. The image is subhomogeneous and has no characters, which is what the central-sequence criterion of Kirchberg and Rørdam and the tensor-power theorem of Dadarlat and Toms require. The manuscript states that the exponent depends on the algebra and that no finite tensor power is claimed to absorb the Jiang–Su algebra.
- Source (openai/math repository, commit
7ef5c0c): The Kirchberg–Rørdam character criterion, dated 25 September 2026. - Formalization, as described by the repository. The scope note lean/docs/299.md states that the formalized result proves, for every nonzero unital separable complex C*-algebra and every free ultrafilter, that the norm central-sequence algebra has no nonzero character exactly when the algebra is isomorphic to its minimal tensor product with the Jiang–Su algebra. The scope note does not mention the tensor-power corollary. The Comparator statement is
CharacterCriterion.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | The character criterion: full cones and dimension drop, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains characters and central sequences, the criterion, positive comparison and finite tests that survive every representation, the matrix cone and cube construction, the conversion to dimension drop, and the application to central sequences, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": the Lean statement is the character criterion, while the infinite tensor-power result is not stated. It notes that the Jiang–Su algebra, the norm ultrapower, the minimal tensor product and the central subalgebra are hand-built models rather than Mathlib definitions, so the formal isomorphism is only as faithful as these models. It records a Comparator pass on cloud machines for CharacterCriterion, finished on 8 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the CharacterCriterion solution, in 1349 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 | C. Toledo, OpenAI's math release: what it claims beyond what it checks | Review (scope of the formal statements) | Lists this family among those whose compared formal statement is narrower than the manuscript's claims without saying so, because the infinite tensor-power conclusion is not formalized; findings dated 10 October 2026 at repository commit fd4aeeb. |
Self-published report by the author of cert-machine. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list CharacterCriterion, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-14 | Characters of central sequences and Jiang–Su stability, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Six lessons on the positive answer to the question of Kirchberg and Rørdam. The core finite theorem, that a nonzero unital C*-algebra without characters has a finite tensor power receiving a unital homomorphism from the dimension-drop algebra I(2,3), is proved in full; the theorems of Kirchberg and Rørdam and of Dadarlat and Toms are named hypotheses. | The lessons state that they were written by Claude Opus 5.5 (Anthropic) in October 2026 and self-checked by the writing AI; the course lists its status as author self-checked. |
| 2026-10-18 | AI Proved What?, episode 299 No characters, then Z-stable?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim. The episode states that no finite tensor power is claimed to be Jiang–Su stable, that no bound on the power is claimed, and that nothing is claimed for non-unital algebras; it reports that a problem list still carried the question in May 2026. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 21 pages, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: in part, the main criterion and not the tensor-power result. The page states that it found no expert comment. |
| 2026-10-20 | C. Bruce and S. Geffen, C*-selflessness and 𝒵-stability for Thompson's group F (arXiv:2610.28473, v1) | Use | Proves that the reduced group C*-algebra of Thompson's group F is Jiang–Su stable and selfless. The Jiang–Su stability proof uses the manuscript's corollary that the infinite minimal tensor power of every nonzero unital separable C*-algebra without characters contains a unital copy of the Jiang–Su algebra; it also uses a second OpenAI manuscript, on the nonamenability side, see Thompson's group F is nonamenable. | arXiv preprint, version 1, marked preliminary. The authors state that GPT-6 Astra, GPT-6.1 Sol, Claude Opus 5.5 and Claude Fable 5.1 were used to produce first drafts of proofs, suggest improvements and proofread, and that the authors verified every proof. |
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.
