Papers With

← All papers
First page of A separably representable counterexample to Naimark's problem in ZFC

A separably representable counterexample to Naimark's problem in ZFC

Ryotaro Tanaka

math.OA Sep 22, 2026 · v1 math.FA
formalization mathlib analysis ai-agents
Read PDF arXiv abstract Code
TL;DR
Main results (irreducible-representation classification, unique trace extension, separable faithful model, density/CH statements) are formalized in Lean 4 with Mathlib in MathlibAnnex.
Abstract
We construct in ZFC a unital, simple, infinite-dimensional $C^*$-algebra whose nonzero irreducible representations form a single unitary equivalence class, but which admits a faithful representation on a separable Hilbert space. The algebra contains a unital copy of the canonical anticommutation relation (CAR) algebra, and the normalized CAR trace has a unique extension among all states. This extension is tracial, and its GNS representation is separable and faithful, with weak closure the hyperfinite $\mathrm{II}_1$ factor. In contrast, every nonzero irreducible representation acts on a Hilbert space of density $2^{\aleph_0}$. The construction separates the added unitaries into shell terms, controlled by finite CAR relations, and rank-one defect terms. These relations determine every irreducible representation of the generated algebra and every extension of the CAR trace. The algebra has norm density $2^{\aleph_0}$; consequently, the continuum hypothesis (CH) is equivalent over ZFC to the existence of a counterexample to Naimark's problem of norm density $\aleph_1$.
Problem

Naimark's problem asks whether a C*-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. Earlier counterexamples needed extra set-theoretic hypotheses such as Jensen's diamond principle.

Approach

The authors build in ZFC a unital simple C*-algebra generated by a copy of the CAR algebra and added unitaries. Each added unitary is split into shell terms, controlled by finite CAR relations through decreasing pure-state projections, and rank-one defect terms. These relations determine every irreducible representation and every state extension of the CAR trace. The main statements are formalized in Lean 4 on top of Mathlib in the MathlibAnnex project. The formalization matches results, not proofs line by line, and was developed with ChatGPT and Codex assistance.

Results

The algebra has a single unitary equivalence class of nonzero irreducible representations, all acting on Hilbert spaces of density 2^aleph0, yet it has a faithful separable tracial representation whose weak closure is the hyperfinite II_1 factor. Consequently, CH is equivalent over ZFC to the existence of a counterexample of norm density aleph_1. The Lean release passes axiom checks restricted to propext, Classical.choice and Quot.sound. The weak-closure corollary is not formalized.