Amenability, unitarizability, and strong Ulam stability

2 papersLean

Resolves Dixmier's problem for all discrete groups: amenability is equivalent to every uniformly bounded Hilbert-space representation being similar to a unitary representation. For countable discrete groups, amenability is also equivalent to strong Ulam stability: sufficiently accurate unitary approximate representations are uniformly close in operator norm to genuine representations on the same, possibly infinite-dimensional, Hilbert space.

Watch

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation

▶The proposed solutionin preparation

Papers 2

Unitarizability implies amenability for discrete groups

OpenAI · September 23, 2026

We prove that a discrete group is amenable if and only if every uniformly bounded representation on a complex Hilbert space is similar to a unitary representation. This resolves Dixmier's unitarizability problem affirmatively for discrete groups.

Read PDF Download Source

Cite

@misc{OAI:Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026,
  author = {{OpenAI}},
  title = {{Unitarizability implies amenability for discrete groups}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026/paper.pdf}{OAI:Unitarizability-Implies-Amenability-for-Countable-Groups-September-23-2026}},
  year = {2026}
}

Strong Ulam Stability Characterizes Amenability

OpenAI · October 5, 2026

A countable discrete group is amenable if and only if it is strongly Ulam stable: every sufficiently accurate unitary almost representation, on any complex Hilbert space, is uniformly close in operator norm to a genuine representation on the same space. We prove the converse to Kazhdan's amenable stability theorem, answering the question of Burger, Ozawa, and Thom. The inclusion of infinite-dimensional Hilbert spaces is essential.

Read PDF Download Source

Cite

@misc{OAI:Strong-Ulam-Stability-Characterizes-Amenability-October-5-2026,
  author = {{OpenAI}},
  title = {{Strong Ulam Stability Characterizes Amenability}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Strong-Ulam-Stability-Characterizes-Amenability-October-5-2026/strong-ulam-stability.pdf}{OAI:Strong-Ulam-Stability-Characterizes-Amenability-October-5-2026}},
  year = {2026}
}

What was formalized in Lean

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

Unitarizability implies amenability for discrete groups

Scope

Dixmier's unitarizability problem asks whether a discrete group is amenable exactly when every uniformly bounded Hilbert-space representation is similar to a unitary one. The formalization establishes this equivalence for every discrete group.

For every nonamenable group and every \(\varepsilon>0\), it also gives a nonunitarizable representation with uniform operator bound at most \(1+\varepsilon\). The Hilbert space can be chosen separable for countable groups; a separate linked statement records a separable witness with uniform bound \(101\) in that case.

Comparator links

Result	Comparator statement
Unitarizability for all discrete groups	DixmierAllDiscrete.lean
Separable nonunitarizable witnesses for countable nonamenable groups	Dixmier.lean

Scope note on GitHub →