Kirchberg's $\mathcal O_2$ norm-ultrapower embedding problem

Proves, with a Lean check, an explicit C*-algebra that fits in no nuclear norm ultrapower, answering Kirchberg.

1 paper September 23, 2026 Explained by AI

Every separable exact C*-algebra fits inside one universal algebra, the Cuntz algebra O₂. Kirchberg asked whether every separable C*-algebra at least fits inside an ultrapower of O₂, a much larger limit of copies of it. This paper answers no, with an explicit algebra built from a concrete group. The algebra does not fit unitally into the ultrapower of any nonzero unital nuclear algebra. Lean checks the main theorem.

First step

2000

Eberhard Kirchberg and N. Christopher Phillips, embedding of exact algebras into O₂

Significance

Major

It answers Kirchberg's norm-ultrapower embedding problem negatively with an explicit counterexample.

Trust

Formal proof listed

Field

Operator algebras

1 paper

The explanation

Number the slots of an infinite list 0, 1, 2, and so on. Define one operator that moves slot n to slot 2n, and another that moves it to 2n + 1. Slot 5 goes to 10 under the first and to 11 under the second. Each operator keeps lengths, so it is an isometry. Together their images cover every slot exactly once, the even ones and the odd ones. That is the rule s₁s₁* + s₂s₂* = 1. The algebra these two generate is the Cuntz algebra O₂.

O₂ is surprisingly universal. Kirchberg and Phillips showed that every separable unital exact C*-algebra embeds unitally into O₂Source 1. A C*-algebra is an algebra of operators closed under adjoints and norm limits. Exactness is a mild tameness property. The question is what happens without exactness. An ultrapower O₂^ω is a huge algebra built from bounded sequences of elements of O₂. Two sequences count as equal when they get close along a chosen limit, an ultrafilter. Kirchberg asked whether every separable unital C*-algebra embeds unitally into O₂^ωSource 2. It is a different question from Connes' embedding problemSource 3. The obstacle is that O₂^ω is very roomy. It even contains isometries that are not onto, so simple size arguments failSource 4.

This paper gives a negative answerSource 5. It takes vectors of three numbers whose entries are fractions with powers of 2 below. The group combines these vectors with 3-by-3 integer matrices of determinant 1 and doubling. Its full group C*-algebra does not embed unitally into O₂^ωSource 6. The group does not depend on the target algebra or the ultrafilterSource 7. It works for every nonzero unital nuclear target.

The inner part of the group, with integer vectors, has property (T), a strong rigidity conditionSource 8. Doubling sends it onto a subgroup of index eightSource 9. For example, the vector (1, 0, 3) goes to (2, 0, 6). Integer vectors fall into 2 × 2 × 2 = 8 classes by the parity of each entry. Doubled vectors fill only the all-even class. The proof tracks finite-dimensional representations of the inner group inside a nuclear algebra. Only finitely many types can appear. Doubling would force an endless chain of new types, a contradiction.

How sure is this? A computer proof checker called Lean has a formal proof. It builds the explicit separable unital full group C*-algebra. It shows the algebra has no unital embedding into B^ω for any nonzero unital nuclear B and any free ultrafilter. No specialist review of the paper has been published.

What it doesn't show. This does not settle Connes' embedding problem or the tensor-norm form of Kirchberg's conjecture, which are different questions.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

Major: it answers Kirchberg's embedding problem with an explicit example, and Lean formally checks the main theorem. No specialist review is published.

Words used

C*-algebra: An algebra of operators on a Hilbert space, closed under adjoints and norm limits.
Cuntz algebra O₂: The algebra generated by two isometries whose ranges split the space in two, like even and odd slots.
Exact: A tameness property: tensoring with the algebra preserves short exact sequences.
Nuclear: Well approximated by finite matrix algebras, in a precise sense; O₂ is nuclear.
Norm ultrapower B^ω: Bounded sequences in B, with two sequences identified when their difference shrinks along a chosen limit.
Free ultrafilter: A consistent rule for choosing which infinite sets of indices count as large, used to take limits.
Property (T): A rigidity condition: representations with almost-invariant vectors have truly invariant ones.
Full group C*-algebra: The largest C*-algebra built from all unitary representations of a group.

The original paper

An explicit obstruction to nuclear norm-ultrapower embeddings (PDF, opens in a new tab)
September 23, 2026

Lean notes

All quoted lines (9)

The embedding theorem of Kirchberg–Phillips states that every separable unital exact $C^*$ -algebra embeds unitally into $\Otwo$ .
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
Kirchberg's embedding problem asks whether every separable unital $C^*$ -algebra admits a unital embedding into $\Otwo^\omega$ ; see Goldbring–Sinclair.
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
It is distinct from the tensor-norm formulation of Kirchberg's conjecture and from Connes' embedding problem, as emphasized in.
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
The target class here is different: nonfiniteness of $C^*(G)$ alone cannot exclude a unital embedding into $\Otwo^\omega$ , which itself contains proper isometries.
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
We give a negative answer to Kirchberg's norm-ultrapower embedding problem.
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
In particular, $A$ does not embed unitally into $\Otwo^\omega$ .
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
The group is countable and independent of both $B$ and $\omega$ ; no separability assumption on $B$ is needed.
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
The subgroup $\Gamma=\Z^3\rtimes\SL_3(\Z)$ of $G$ has property (T).
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text
Conjugation by the generator $t$ of the last $\Z$ -factor sends $\Gamma$ onto the index-eight subgroup $\theta(\Gamma)$ , where $\theta(v,M)=(2v,M)$ .
An explicit obstruction to nuclear norm-ultrapower embeddings Back to text

Other sources

openai/math, Lean scope note for family 292 The formalization constructs an explicit separable unital full group $C^*$ -algebra that has no unital embedding into $B^\omega$ for any nonzero unital nuclear $C^*$ -algebra $B$ and any free ultrafilter $\omega$ on $\mathbb N$ .
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

297A ZFC counterexample to Naimark's problemOperator algebras
302Radius of comparison equals half the mean dimensionOperator algebras
303Weak pure infiniteness and Cuntz-algebra absorptionOperator algebras
291Cuntz comparison, nuclear dimension, and equivariant Jiang–Su stabilityOperator algebras
293Invariant projections, hyperinvariant subspaces, and transitive algebrasOperator algebras

Browse Operator algebras Open since the 2000s Lean-checked results

Kirchberg's O2\mathcal O_2O2​ norm-ultrapower embedding problem