Constructs an infinite finitely presented simple amenable group, answering the longstanding question of whether these properties can occur simultaneously. (Lean)
Manuscript
An infinite finitely presented simple amenable group
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026}
We construct an infinite finitely presented simple amenable group, giving a positive answer to the finite-presentation existence question for simple amenable groups.
Result 253 · Group theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md