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

• ams-20

Choose either option

• I plan on adding this conjecture to the repository
• 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

Feedback on mistakes/hallucinations: link