Dixmier's unitarizability problem for discrete groups
A representation of a discrete group on a Hilbert space is uniformly bounded if , and unitarizable if some bounded invertible makes every unitary; is unitarizable if every uniformly bounded representation is. Day and Dixmier (1950) showed amenable groups are unitarizable, and groups containing a nonabelian free subgroup are not (Ehrenpreis-Mautner, Pytlik-Szwarc). Partial converses were known via Pisier's quantitative criterion, Epstein-Monod, Osin, Monod-Ozawa and Vergara. Dixmier asked whether unitarizability characterizes amenability: is every unitarizable discrete group amenable?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Group theory; amenability and uniformly bounded representations
- Posed by
- Jacques Dixmier, Les moyennes invariantes dans les semi-groupes et leurs applications, Acta Sci. Math. (Szeged) 12 (1950), section 5, p. 221
- Year posed
- 1950
- Years open
- 76y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 55 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: a discrete group is amenable if and only if every uniformly bounded representation on every complex Hilbert space is similar to a unitary one. For every nonamenable and there is a representation with not similar to a unitary one, on a separable space if is countable. This settles Dixmier's question for all discrete groups. Not shown: anything for nondiscrete locally compact groups, or a bound on similarity degree beyond what the theorem gives.
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscripts are authored 'OpenAI' and name no human author. The principal manuscript (September 23, 2026) proves the main equivalence without companion inputs, per its INPUTS.md; only a side consequence for group C*-algebras uses the release's Kadison similarity manuscript.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 of 'Unitarizability implies amenability for discrete groups' was read against Dixmier's question as cited (1950, section 5). The proof (a bounded non-inner operator cocycle built from sparse assignments and random-sign matrix weights) was not refereed. Lean: lean/formalization.yaml lists comparator config ComparatorChallenges/DixmierAllDiscrete.json, declaration OAI.Dixmier.current_main_theorem in OAI/Analysis/Unitarizability/AllDiscrete.lean, permitted axioms propext, Classical.choice and Quot.sound. The statement file was read: for every discrete group, amenability (a positive normalized left-invariant mean on bounded functions) is equivalent to every uniformly bounded representation on every complete complex inner product space being similar to an isometric one, and every nonamenable group has a nonunitarizable representation with bound at most 1 + epsilon, on a separable space when the group is countable. That is the headline claim. A second challenge, ComparatorChallenges/Dixmier.json (countable groups, separable witness with bound 101, solution module OAI/Analysis/Unitarizability/UniverseTransport.lean, present at the commit), is not in the formalization catalogue; its statement was read here. Neither was rebuilt here.