Finiteness of Finitely Presented Periodic Groups

### What is the conjecture

A **periodic group** is a group in which every element has finite order. A **finitely presented group** is a group that can be described using a finite set of generators and finitely many relations between them.

The conjecture asks: If $G$ is a finitely presented group and $G$ is periodic, must $G$ be finite?

Equivalently: Does there exist a finitely presented group $G$ such that $G$ is periodic but $G$ is infinite?

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Periodic_group, https://en.wikipedia.org/wiki/Presentation_of_a_group, Olshanskii, A. Yu. (1991). Geometry of defining relations in groups (Mathematics and Its Applications), Hall, M. (1959). The theory of groups (Macmillan)

### Prerequisites needed

**Formalizability Rating:** 1.5/5 (0 is best) (as of 2026-02-03)

Building blocks (1-3; from search results):
- `Group` and finite order concepts (via `orderOf` in `Mathlib.GroupTheory.OrderOfElement`)
- `Finite` and `Fintype` for finiteness predicates
- Basic group theory infrastructure in Mathlib

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of "finitely presented group" (not a standard Mathlib predicate; would need to formalize group presentations or an equivalent characterization)
- Formal definition of "periodic group" (needs to characterize: every element has finite order; can be expressed as `∀ g : G, ∃ n : ℕ, n ≠ 0 → g ^ n = 1` using existing tools)

Rating justification (1-2 sentences): The core group-theoretic machinery (group definitions, finite order, finiteness) exists in Mathlib, but "finitely presented" requires formalization as a definition on presentations or as a computable predicate. This moderate infrastructure gap results in a rating of 3.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-20

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)