OpenAI claims Kadison’s similarity problem (Lean)

Your AI and this story

Key facts

• Claim (abstract, verbatim): ‘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.’
• Scope (paper, after Theorem 1.1): ‘The theorem imposes no separability, nuclearity, finite generation, faithfulness, or normality condition.’ The similarity may depend on the homomorphism; the paper does not claim an a priori bound on its condition number
• Earlier results, as the paper recounts them: the nuclear case (Bunce, Christensen); cyclic representations, and C*-algebras without tracial states (Haagerup, 1983); type II₁ factors with property Γ (Christensen); Kirchberg’s equivalence of the similarity property with innerness of derivations; Pisier’s similarity degree; Eleftherakis and Paulsen’s equivalence with the statement that every von Neumann algebra is hyperreflexive
• Route (paper §1.2): Theorem 1.2 gives an absolute constant C with ‖[Y⁽ʰ⁾, X]‖ ≤ C·g_P(Y)·‖X‖ for every von Neumann algebra P, every operator Y, every matrix size h and every X ∈ M_h(P). The hard case is finite factors, ‘where the estimate must be uniform in the factor and its representation multiplicity’. It is handled through a tracial free product, Schur–Weyl duality and Popa’s relative independence theorem in ultrapowers; Paulsen’s theorem and Kirchberg’s equivalence then give similarity
• Lean scope note (lean/docs/288.md): ‘The formalization proves this for arbitrary Hilbert spaces. It also gives one universal hyperreflexivity constant for all unital von Neumann algebras.’ In the comparator file KadisonSimilarity.lean, a bounded unital homomorphism is a continuous ℂ-algebra map from a Mathlib C*-algebra into B(H), and similarity means an invertible S with Sπ(a*)S⁻¹ = (Sπ(a)S⁻¹)*. Our reading: this is Kadison’s problem as usually stated. The constant is explicit: the hyperreflexivity bound is 2·universalConstant, about 2.4 million by our arithmetic from the file’s definitions
• Machine checks: KadisonSimilarity and UniformCommutator were accepted in the oai-math-revised comparator run of 25–26 Oct (‘Lean default kernel accepts the solution’, standard axioms only, no definition-body caveat for these configurations). MathVet rates the formal statement ‘full’ with a sandboxed comparator pass, a verdict it calls ‘pre-referee: one model-assisted reading per family, validated mechanically, not yet re-read by a named human referee’
• Trackers: Matthew Colbrook’s AIM list marks problem 037 ‘Kadison’s similarity problem’ SOLVED (13 Oct), on what it calls ‘an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay’. Jesse Peterson’s list of open problems in operator algebras, last updated on 15 May 2026, before the release, lists it as Problem O.5
• Reactions: none from operator algebraists found as of 29 Oct. We searched the web, arXiv, Hacker News and Proofs and Prompts’ collection of 100+ reactions; the oai-math-revised notes report ‘Follow-up works: None found’. The same release also claims other problems on Peterson’s list: the generator problem (family 296), the free group factor problem (287), strong Kadison–Kastler (289) and the Kadison–Ringrose vanishing-cohomology conjecture (295)