# Kadison's similarity conjecture

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

- [Kadison's similarity theorem through uniform derivation estimates](../../preprints/Kadisons-similarity-theorem-through-uniform-derivation-estimates-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Kadison's similarity theorem and uniform hyperreflexivity | [KadisonSimilarity.lean](../ComparatorChallenges/KadisonSimilarity.lean) |
| Uniform amplified commutator estimate | [UniformCommutator.lean](../ComparatorChallenges/UniformCommutator.lean) |