Back to Problems

bounded_burnside_problem

Specification

Let $G$ be a finitely generated group, and assume there exists $n$ such that for every $g$ in $G$, $g^n = 1$. Is $G$ necessarily finite?

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem bounded_burnside_problem :
    answer(sorry) ↔ ∀ (G : Type) [Group G] (fin_gen : Group.FG G)
      (n : ℕ) (hn : n > 0) (bounded : ∀ g : G, g^n = 1), Finite G
ID: Wikipedia__BoundedBurnsideProblem__bounded_burnside_problem
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.