Prove Dixmier (openai/math family 251: Amenability, unitarizability, and Ulam stability) in Lean 4 with…
Prove Dixmier (openai/math family 251: Amenability, unitarizability, and Ulam stability) in Lean 4 with…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 251 of the release, Amenability, unitarizability, and Ulam stability (Group theory)…
The task
Context: this statement belongs to family 251 of the release, *Amenability, unitarizability, and Ulam stability* (Group theory). The family as a whole: Resolves Dixmier's problem for all discrete groups: amenability is equivalent to every uniformly bounded Hilbert-space representation being similar to a unitary…
Part of raising-heart/openai-math.