we-solve (beta)

Math-380-A2 · revision r1 · on Math-380

OpenAI claim summary for Math-380

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The source equates amenability and unitarizability for all discrete groups, hence proves the target implication. Its construction of nonunitarizable representations with arbitrarily small excess uniform bound strengthens the converse direction.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. The Dixmier Unitarisability Problem
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

The Dixmier Unitarisability Problem

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. Discrete-group amenability is claimed equivalent to unitarizability of all uniformly bounded complex Hilbert representations.

Mathematical statement of the claimed result

Result 1.
A uniformly bounded representation $\pi:G\to\operatorname{GL}(\mathcal K)$ is unitarizable when it is similar to a unitary representation. The source claims for every discrete group \[ G\text{ amenable}\quad\Longleftrightarrow\quad G\text{ unitarizable}. \] Its strengthened assertion says that for every nonamenable $G$ and every $\varepsilon>0$, there is a nonsimilar-to-unitary representation satisfying \[ \sup_{g\in G}\|\pi(g)\|\le1+\varepsilon. \] For countable $G$, the witnessing complex Hilbert space may be separable; countability is not required for the equivalence.

Outline of the argument

Nonamenability supplies sparse assignments that are turned into weighted block operators. Their invariant-kernel obstruction rules out a similarity to unitaries for the constructed bounded representation, giving the converse to the established amenable implication.

Formal verification

For family 251, the documented theorem gives amenability--unitarizability equivalence for arbitrary discrete groups and almost-unitary nonunitarizable witnesses; countable groups have separable witnesses. The later strong-Ulam theorem is not selected. The listed Comparator files are Dixmier.lean, DixmierAllDiscrete.lean. Named declarations include OAI.Dixmier.current_main_theorem. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources