Kirchberg's embedding problem
From OpenAI Aftermath
Kirchberg's embedding problem asks whether every separable C*-algebra embeds into the norm ultrapower of the Cuntz algebra O2, which would make O2 able to approximate every separable C*-algebra in operator norm. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 23 September 2026, claims a negative answer through an explicit full group C*-algebra. This page summarizes the published claim 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:
- The embedding theorem of Kirchberg and Phillips states that every separable unital exact C*-algebra embeds unitally into O2. Kirchberg asked whether every separable unital C*-algebra embeds unitally into the norm ultrapower O2ω, as recounted by Goldbring and Sinclair, who also note that the question is distinct from the tensor-norm formulation of Kirchberg's conjecture and from Connes' embedding problem.
- Fox, Goldbring and Hart derived computability-theoretic consequences of a positive answer. Goldbring and Sinclair gave a conditional route to a negative answer through a weakly explicit minimal tensor norm, a property of O2 that they left open.
- Sauers and Eckhardt used the same ascending HNN extension to show that its full group C*-algebra contains a proper isometry and to construct groups that are not MF. The manuscript notes that nonfiniteness alone cannot exclude an embedding into O2ω, which itself contains proper isometries.
The original result
- Claim. Theorem 1.1 of An explicit obstruction to nuclear norm-ultrapower embeddings states that for the group G = Z[1/2]3 ⋊ (SL3(Z) × Z), in which (M, k) acts by v ↦ 2kMv, the full group C*-algebra C*(G) admits no unital embedding into Bω for any nonzero unital nuclear C*-algebra B and any free ultrafilter ω on the natural numbers. Taking B = O2 gives the negative answer to Kirchberg's problem; the manuscript notes that the unital formulation is equivalent to the one without unit preservation.
- Further claims. A corollary states that neither O2 nor any exact or nuclear unital C*-algebra is existentially closed among unital C*-algebra extensions, that O2ω-embeddability is not preserved by crossed products by Z, and that some satisfiable finite condition lacks good nuclear witnesses.
- Method, as described: the subgroup Z3 ⋊ SL3(Z) has property (T), and conjugation by the generator of the last factor maps it onto a subgroup of index eight, with a finite-dimensional irreducible representation that is inequivalent to all its compositions with this self-embedding. For coordinate lifts of a hypothetical embedding, a spectral test with a fixed threshold defines a set of representation classes; a finiteness lemma for approximate finite-dimensional representation types inside a nuclear algebra, following Wassermann's tensor-product method, makes this set finite, and the spectral gap forces a chain of predecessors that must repeat, contradicting the inequivalence.
- Source (openai/math repository, commit
7ef5c0c): An explicit obstruction to nuclear norm-ultrapower embeddings, dated 23 September 2026. - Formalization, as described by the repository. The scope note lean/docs/292.md states that the formalization constructs the explicit separable unital full group C*-algebra with no unital embedding into Bω for any nonzero unital nuclear B and any free ultrafilter ω, and in particular none into an ultrapower of O2. It links the comparator statement NuclearUltrapower.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 28 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Nuclear ultrapowers: a finite spectral obstruction, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains the claimed explicit obstruction: nuclear approximation and norm ultrapowers, a spectral test for representation types, the finiteness of approximate matches forced by nuclearity uniformly in the matrix dimension, finite-index transport and the predecessor relation, and the finite chain that gives the contradiction, with the consequences and their verification boundaries. | 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-14 | Kirchberg's embedding problem, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Three lessons: norm ultrapowers and a group with property T; a spectral test and nuclear finiteness; and predecessors and the contradiction. | 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 292 Too big for the hotel?, remade version of 23 October 2026 | Reading (exposition) | Video explainer of the claim that the full group C*-algebra of the semidirect product of Z[1/2]³ by SL₃ of the integers times Z does not embed unitally in any norm ultrapower of any nonzero unital nuclear C*-algebra, so that Kirchberg's question whether every separable C*-algebra embeds in the norm ultrapower of O₂ has a negative answer. The episode states that nothing is claimed about trace-based ultrapowers, the reduced group C*-algebra or targets that are not nuclear. | 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, 14 pages, dated September 23, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the full theorem, with the O₂ corollary. The page also states that the Lean formalization of the full theorem with the O₂ corollary has about 18,500 lines with no unproved steps in the site's scan, without building it, that its proof of property T rests on an integer certificate whose residual the site recomputed exactly and matched with the Lean value, that OSVerify has not reviewed the paper and that the site found no expert comment. |
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.
