∑math20

Operator algebras · Result 288

Kadison's similarity conjecture

1 paperLean

Proves Kadison's similarity conjecture: every bounded complex-linear unital algebra homomorphism from a unital complex C∗-algebra to operators on a Hilbert space becomes a \(*\)-homomorphism after conjugation by a bounded invertible operator.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Kadison's similarity theorem through uniform derivation estimates

Kadison's similarity theorem through uniform derivation estimates

OpenAI · September 23, 2026

We prove that every bounded complex-linear unital algebra homomorphism from a unital complex C∗-algebra into the bounded operators on an arbitrary Hilbert space is similar to a \(*\)-homomorphism. This resolves Kadison's similarity conjecture positively. We also obtain one universal hyperreflexivity constant for all unital von Neumann algebras on arbitrary complex Hilbert spaces.

Read PDF Download Source

Cite
@misc{OAI:Kadisons-similarity-theorem-through-uniform-derivation-estimates-September-23-2026,
  author = {{OpenAI}},
  title = {{Kadison's similarity theorem through uniform derivation estimates}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Kadisons-similarity-theorem-through-uniform-derivation-estimates-September-23-2026/paper.pdf}{OAI:Kadisons-similarity-theorem-through-uniform-derivation-estimates-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

Kadison's similarity problem asks whether every bounded unital homomorphism from a unital complex \(C^*\)-algebra into operators on a Hilbert space is similar to a \(*\)-homomorphism. The formalization proves this for arbitrary Hilbert spaces. It also gives one universal hyperreflexivity constant for all unital von Neumann algebras.

The linked commutator estimate is uniform over all finite matrix amplifications: its constant is independent of the algebra, Hilbert space, and amplification size. This is the quantitative derivation estimate supporting the similarity result.

Comparator links

ResultComparator statement
Kadison's similarity theorem and uniform hyperreflexivityKadisonSimilarity.lean
Uniform amplified commutator estimateUniformCommutator.lean

Scope note on GitHub →