∑math20

Group theory · Result 253

An infinite finitely presented simple amenable group

1 paperLean

Constructs an infinite finitely presented simple amenable group, answering the longstanding question of whether these properties can occur simultaneously.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of An infinite finitely presented simple amenable group

An infinite finitely presented simple amenable group

OpenAI · 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.

Read PDF Download Source

Cite
@misc{OAI:An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026,
  author = {{OpenAI}},
  title = {{An infinite finitely presented simple amenable group}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026/paper.pdf}{OAI:An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result answers the existence question affirmatively: there is one group that is infinite, finitely presented, simple, and amenable. Amenability is expressed by the Følner condition.

The later general claims about central kernels and enlargements across families are not included.

Comparator links

ResultComparator statement
Infinite finitely presented simple amenable groupSimpleAmenable.lean

Scope note on GitHub →