Bounded Burnside problem

Reference: Wikipedia

theorem bounded_burnside_problem : (∀ (G : Type) [inst : Group G], Group.FG G → ∀ n > 0, (∀ (g : G), g ^ n = 1) → Finite G) ↔ sorry

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?