# An infinite finitely presented simple amenable group

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

- [An infinite finitely presented simple amenable group](../../preprints/An-Infinite-Finitely-Presented-Simple-Amenable-Group-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Infinite finitely presented simple amenable group | [SimpleAmenable.lean](../ComparatorChallenges/SimpleAmenable.lean) |