Motivation

How rigid is a von Neumann algebra inside $B(H)$? If two algebras $M,N\subseteq B(H)$ have unit balls that are uniformly close, must they be the same algebra up to a small change of coordinates? Kadison and Kastler introduced the distance between the unit balls in 1972 (Amer. J. Math. 1972) and asked whether sufficiently close algebras are spatially isomorphic, implemented by a unitary close to the identity. The positive answer for a class of algebras is called (strong) Kadison–Kastler stability. The problem connects perturbation theory, Hochschild cohomology, and Kadison's similarity problem, and it was settled previously only for injective (amenable) algebras, type I algebras, and specific nonamenable examples.

This mission asks for a formal proof of the uniform strong Kadison–Kastler stability theorem stated in an OpenAI preprint dated September 23, 2026 (source): a single tolerance works for all von Neumann algebras on all Hilbert spaces. The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1972 — Kadison and Kastler introduce the metric and prove stability results for type I algebras (Amer. J. Math. 1972).
• 1974–1975 — Phillips proves spatial isomorphism for close type I algebras (Pacific J. Math. 1974); Christensen obtains a conjugating unitary near the identity (J. LMS 1975).
• 1977 — Christensen (Invent. Math. 1977), Johnson (Proc. LMS 1977) and Raeburn–Taylor (JFA 1977) settle the injective case.
• 1980 — Christensen's theory of near inclusions (Acta Math. 1980).
• 1982 — Johnson's examples show that for C*-algebras the implementing unitary cannot always be chosen near the identity in a uniform way (Canad. Math. Bull. 1982).
• 1983 — Haagerup's cyclic similarity estimate (Ann. of Math. 1983).
• 2010–2012 — Christensen, Sinclair, Smith, White and Winter prove spatial isomorphism for close separable nuclear C*-algebras (PNAS 2010; Acta Math. 2012).
• 2012–2014 — Cameron, Christensen, Sinclair, Smith, White and Wiggins construct the first nonamenable Kadison–Kastler stable factors, $(L^\infty(X)\rtimes SL_n(\mathbb Z))\bar\otimes R$ for $n\ge3$ (PNAS 2012; Duke 2014).
• September 2026 — The OpenAI preprint claims uniform stability for all von Neumann algebras (Theorem 1.1, p. 2).

Setting

Let $H$ be a complex Hilbert space and $B(H)$ the bounded operators with the operator norm. A von Neumann algebra $M\subseteq B(H)$ is a unital $*$-subalgebra equal to its double commutant (in particular it contains the identity $I_H$). Write $M_1=\{x\in M:\|x\|\le1\}$ for its unit ball. The Kadison–Kastler distance is the Hausdorff distance of unit balls,

$$d(M,N)=\max\Bigl(\sup_{x\in M_1}\inf_{y\in N_1}\|x-y\|,\ \sup_{y\in N_1}\inf_{x\in M_1}\|x-y\|\Bigr).$$

A unitary $u\in B(H)$ conjugates $M$ to $N$ if $uMu^*=N$.

Formalization targets

Goal: Theorem 1.1 (p. 2)

For every $\varepsilon>0$ there is $\delta>0$ such that for every complex Hilbert space $H$ and all von Neumann algebras $M,N\subseteq B(H)$ with $d(M,N)<\delta$, there is a unitary $u\in B(H)$ with

$$uMu^*=N\qquad\text{and}\qquad\|u-I_H\|<\varepsilon .$$

The tolerance $\delta$ depends only on $\varepsilon$: not on the algebras, their type, their representations, or the size of $H$.

Significance

The result itself. It answers the Kadison–Kastler perturbation question in its strongest uniform form for von Neumann algebras, including all nonamenable and type III cases and non-separable Hilbert spaces. Consequences include that every algebraic or analytic invariant preserved by unitary conjugacy (type, factoriality, property $\Gamma$, Cartan subalgebras) is locally constant in the Kadison–Kastler metric. The analogous C*-algebra statement fails in its uniform-unitary form by Johnson's examples, so the theorem is specific to von Neumann algebras.

Formalizing it. The statement uses only Mathlib's VonNeumannAlgebra, unitary operators and Hausdorff distance, so it is fully expressible today. The proof, however, draws on free probability, tracial ultraproducts, Tomita–Takesaki theory, crossed products, Poisson boundaries and measurable cocycles, most of which are absent from Mathlib. Formalizing even the amenable (injective) case would be a substantial reusable contribution.

Difficulty

Closeness of unit balls supplies nearby elements but no linear or multiplicative correspondence between the algebras, and it gives no control at matrix levels, where perturbation arguments naturally live. For nonamenable algebras the classical route through vanishing Hochschild cohomology is unavailable. The preprint proceeds by cases. For finite factors it proves a uniform bound on all matrix amplifications of commutator maps (Theorem 3.1, p. 11) and corrects nearby unitaries to a measurable cocycle over an amenable boundary action (Section 4). Infinite factors require comparing modular groups through Tomita graphs (Proposition 6.5, p. 41) and aligning the modular action (Proposition 7.1, p. 45) before passing to crossed products (Theorem 8.4, p. 59). General algebras then require aligning centers and passing from separable to arbitrary Hilbert spaces (Section 9) without losing uniformity.

Formalization scope

• $H$ ranges over complex Hilbert spaces (NormedAddCommGroup, InnerProductSpace ℂ, CompleteSpace) in a fixed universe u; $\delta$ is chosen before $H$, so the uniformity over Hilbert spaces is part of the statement.
• VonNeumannAlgebra H is Mathlib's notion; these algebras contain the identity, so "unital with identity $I_H$" is built in.
• kkDistance M N is Metric.hausdorffDist of the closed unit balls. Both balls contain $0$ and are bounded, so the Hausdorff distance is finite and the definition is exactly (1.1).
• NearConjugacy M N ε asks for a unitary $v$ with $v\,M\,v^*=N$ as sets and $\|v-1\|<\varepsilon$.
• There is no trivializing reading: the hypotheses are satisfied by $M=N$, and the conclusion is nontrivial for $M\neq N$.

Selected references

• OpenAI, Universal strong Kadison–Kastler stability, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Universal-strong-Kadison-Kastler-stability-September-23-2026/paper.pdf
• R. V. Kadison, D. Kastler, Perturbations of von Neumann algebras. I. Stability of type, Amer. J. Math. 94 (1972). https://doi.org/10.2307/2373592
• E. Christensen, Perturbations of type I von Neumann algebras, J. London Math. Soc. (1975). https://doi.org/10.1112/jlms/s2-9.3.395
• E. Christensen, Perturbation of operator algebras, Invent. Math. 43 (1977). https://doi.org/10.1007/BF01390201
• B. E. Johnson, Perturbations of Banach algebras, Proc. London Math. Soc. (1977). https://doi.org/10.1112/plms/s3-34.3.439
• I. Raeburn, J. L. Taylor, Hochschild cohomology and perturbations of Banach algebras, J. Funct. Anal. (1977). https://doi.org/10.1016/0022-1236(77)90072-6
• E. Christensen, Near inclusions of C-algebras*, Acta Math. 144 (1980). https://doi.org/10.1007/BF02392125
• B. E. Johnson, A counterexample in the perturbation theory of C-algebras*, Canad. Math. Bull. 25 (1982). https://doi.org/10.4153/CMB-1982-043-4
• U. Haagerup, Solution of the similarity problem for cyclic representations of C-algebras*, Ann. of Math. 118 (1983). https://doi.org/10.2307/2007028
• E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, W. Winter, Perturbations of nuclear C-algebras*, Acta Math. 208 (2012). https://doi.org/10.1007/s11511-012-0075-5
• J. Cameron, E. Christensen, A. M. Sinclair, R. R. Smith, S. A. White, A. D. Wiggins, Kadison–Kastler stable factors, Duke Math. J. 163 (2014). https://doi.org/10.1215/00127094-2819736