# The Kadison–Ringrose cohomology conjecture

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

- [Vanishing of higher bounded Hochschild cohomology](../../preprints/Vanishing-of-higher-bounded-Hochschild-cohomology-September-23-2026/paper.pdf)

## Scope

The formalization proves vanishing of bounded Hochschild cohomology in every degree at least two for a complex von Neumann algebra with coefficients in itself. Every bounded multilinear cocycle of such a degree is the Hochschild differential of a bounded multilinear cochain one degree lower. No separability or type restriction is imposed. The degree-one inner-derivation theorem is outside this selected statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Bounded primitives for all Hochschild cocycles of degree at least two | [KadisonRingrose.lean](../ComparatorChallenges/KadisonRingrose.lean) |