# A ZFC counterexample to Naimark's problem

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A counterexample to Naimark's problem in ZFC](../../preprints/A-counterexample-to-Naimarks-problem-in-ZFC-September-24-2026/naimark-counterexample-zfc.pdf)

## Scope

Naimark's problem asks whether a $C^*$-algebra whose nonzero irreducible representations are all unitarily equivalent must be an algebra of compact operators. The formalization gives a counterexample in ZFC: a unital infinite-dimensional simple complex $C^*$-algebra with a faithful tracial state has that uniqueness property for irreducible representations but is not isomorphic to the compact operators on any Hilbert space. No additional set-theoretic assumption is used.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Counterexample to Naimark's problem in ZFC | [Naimark.lean](../ComparatorChallenges/Naimark.lean) |