Prove UniformGamma (openai/math family 291: Toms–Winter and equivariant Jiang–Su stability) in Lean 4 with…
Prove UniformGamma (openai/math family 291: Toms–Winter and equivariant Jiang–Su stability) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 291 of the release, Toms–Winter and equivariant Jiang–Su stability (Operator…
The task
Context: this statement belongs to family 291 of the release, *Toms–Winter and equivariant Jiang–Su stability* (Operator algebras). The family as a whole: Proves equivariant Jiang–Su stability for every countable discrete amenable group action on a simple separable unital infinite-dimensional nuclear stably finite…
Part of raising-heart/openai-math.