Kadison's similarity theorem through uniform derivation estimates

Formalization

• OpenAI math release, Kadison's similarity conjecture (Lean scope note) (lean/docs/288.md, October 2026). The release's scope note says the formalization covers the similarity theorem for arbitrary Hilbert spaces, the universal hyperreflexivity constant and the uniform amplified commutator estimate (Theorem 1.2), and links the KadisonSimilarity and UniformCommutator comparator statements.
• OpenAI math release, KadisonSimilarity.lean (Comparator challenge statement) (lean/ComparatorChallenges, 2026). This Comparator challenge file states universalCommutatorTheorem, universalHyperreflexivity and similarityTheorem, which correspond to Theorem 1.2, Corollary 1.3 and Theorem 1.1; the statements are left as sorry, which is how Comparator challenge statements are given.

Possibly relevant literature (found by the agent, not checked)

• E. Papapetros, A new approach to the similarity problem (arXiv:2403.19668, 2024; published in Advances in Operator Theory 9, article 65, 2 July 2024). Shows that the hypothesis "every separably acting von Neumann algebra with a cyclic vector is hyperreflexive" implies the similarity property for all C*-algebras, a weaker form of the paper's Corollary 1.3 (universal hyperreflexivity).
• G. K. Eleftherakis and E. Papapetros, The similarity problem and hyperreflexivity of von Neumann algebras (arXiv:2306.07605, 2023; revised 17 January 2024; listed as forthcoming in J. Operator Theory). Characterizes the weak similarity property of a von Neumann algebra by hyperreflexivity of tensor products of its commutant with B(ℓ²(I)), which bears on the hyperreflexivity consequence in Corollary 1.3.
• J. Cameron, E. Christensen, A. M. Sinclair, R. R. Smith, S. White and A. D. Wiggins, A remark on the similarity and perturbation problems (arXiv:1206.5405; C. R. Acad. Sci. Canada 35(2), 2013). Shows that Kadison's similarity problem is equivalent to whether close C*-algebras must have close commutants, so Theorem 1.1 would also have consequences for that perturbation question.
• G. Pisier, A note on strong similarity and the Connes embedding problem (arXiv:2601.10654, Jan–Feb 2026). Constructs a completely bounded homomorphism into a QWEP von Neumann algebra that is not strongly similar to a $*$-homomorphism, which is background on where the similarity $S$ (and the operators implementing derivations via Paulsen's theorem) can be taken to lie.

Digests and expositions

• Gradient Damage, Kadison's Similarity Problem: Every Warped Action Can Be Unwarped (video and accompanying description, 14 October 2026). This 22-second animation illustrates similarity through a stretched rotation action, links the manuscript, and describes the visualization as an illustration rather than a proof.