# An infinite finitely presented residually finite 2-group and a finitely presented nil algebra

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

- [An infinite finitely presented periodic group](../../preprints/An-infinite-finitely-presented-periodic-group-September-23-2026/paper.pdf)

## Scope

The finitely presented Burnside question asks whether a finitely presented group in which every element has finite order must be finite. The formalization gives a negative answer by constructing an infinite finitely presented periodic group, including a witness realized as a Steinberg group over an algebra of characteristic two. Periodicity means that each element has some finite order; no common exponent is asserted. The paper's separate nil-algebra and radical-algebra conclusions are outside these selected statements.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Infinite finitely presented periodic group | [PeriodicGroup.lean](../ComparatorChallenges/PeriodicGroup.lean) |