Prove KadisonRingrose (openai/math family 295: The Kadison–Ringrose cohomology conjecture) in Lean 4 with…
Prove KadisonRingrose (openai/math family 295: The Kadison–Ringrose cohomology conjecture) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 295 of the release, The Kadison–Ringrose cohomology conjecture (Operator algebras)…
The task
Context: this statement belongs to family 295 of the release, *The Kadison–Ringrose cohomology conjecture* (Operator algebras). The family as a whole: Proves that every bounded Hochschild cocycle of degree at least two on a complex von Neumann algebra, with coefficients in the algebra itself, has a bounded primitive.…
Part of raising-heart/openai-math.