Unitarizability implies amenability for discrete groups

Lean formalization in OpenAI math repository (Result 251)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Unitarizability implies amenability for discrete groups'. We prove that a discrete group is amenable if and only if every uniformly bounded representation on a complex Hilbert space is similar to a unitary representation. This resolves Dixmier's unitarizability problem affirmatively for discrete groups.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 251). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository