The finitely presented Burnside problem

The finitely presented Burnside problem asks whether a group with a finite presentation, in which every element has finite order, must be finite. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math) claim a negative answer: an infinite finitely presented periodic group (dated 23 September 2026), and a strengthening to an infinite finitely presented residually finite group in which every element has 2-power order (dated 5 October 2026). This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the introductions of both manuscripts:
  • Burnside (1902) asked whether finitely generated periodic groups must be finite.
  • Golod (1964) answered this negatively for finitely generated groups through the Golod–Shafarevich inequality; his groups are residually finite p-groups.
  • Novikov and Adian (1968) constructed infinite finitely generated groups of bounded exponent.
  • Zel'manov solved the restricted Burnside problem for odd exponents and for powers of two.
• Ol'shanskii and Sapir distinguish the finitely presented periodic-group question explicitly (2003, p. 45). Their finitely presented torsion-by-infinite-cyclic groups are not periodic. The October manuscript also cites Haettel and Osajda (2025, Section 2.2(IX)) for the question.
• Zel'manov's theorem implies that a finitely generated residually finite group of exponent dividing 2^a is finite. A residually finite example of the October kind must therefore have unbounded element orders.

The original results

• Periodic group (23 September 2026). Theorem 1.1: there is a unital associative algebra R over F₂ for which the Steinberg group St₁₂(R) is infinite, finitely presented and periodic. The order of an element may depend on the element.
  • Corollary: the group also has Kazhdan's property (T), by a theorem of Ershov and Jaikin-Zapirain, and hence is nonamenable.
  • Algebra corollaries: an infinite-dimensional finitely presented nonunital nil algebra over F₂ that is Jacobson radical but not nilpotent. The manuscript presents this as negative answers to the finitely presented nil and radical nilpotence questions (attributed to Ufnarovskij and Amitsur), and to the finite-presentation version of Kurosh's question.
• Method, as described in the manuscript. The ring is an infinite finitely presented graded algebra R = F₂ ⊕ I in which every matrix over the positive-degree ideal I is nilpotent. It is built from a finite table of homogeneous word rules that encode a self-similar hierarchy. The manuscript names fixed-point tiling constructions of Durand, Romashchenko and Shen as a close predecessor. The proof then meets four obligations for the same ring:
  • finite presentation of St_n(R), following Krstić and McCool's method;
  • infinitude, from the distinct elementary matrices;
  • periodicity of the elementary matrix group;
  • torsion of the kernel of St₁₂(R) → E₁₂(R).
• Residually finite 2-group (5 October 2026). The October manuscript proves that Γ = St₁₂(R) from the first manuscript is residually finite. Its finite-index subgroup ker(Γ → St₁₂(F₂)) is infinite, finitely presented and residually finite, and every element has finite 2-power order; the orders are unbounded. The abstract describes the mechanism: phases of long words in the graded algebra let finite degree truncations detect every element of Γ.
• Sources. Commit 1581d4c of the openai/math repository:
  • An infinite finitely presented periodic group;
  • An infinite finitely presented residually finite 2-group.
• Formalization, as described by the repository.
  • The scope note lean/docs/247.md states that the formalization gives the negative answer by constructing an infinite finitely presented periodic group, including the Steinberg-group witness over an algebra of characteristic two. "No common exponent is asserted." The nil-algebra and radical-algebra conclusions are outside the selected statements. Residual finiteness and 2-power orders are not among them either.
  • The Comparator challenge PeriodicGroup.lean states thm_main : MainStatement ∧ BurnsideStatement. Here MainStatement asserts an F₂-algebra R with Steinberg 12 R infinite, finitely presented and periodic. BurnsideStatement asserts some infinite, finitely presented, periodic group.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 16 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "weaker-statement" against its summary of a residually finite 2-group: the challenge states only the infinite finitely presented periodic group. It notes that the negative answer to the finitely presented Burnside problem itself is covered. Records a sandboxed Comparator pass for PeriodicGroup.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (tasks #348, #353)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, Lean's official kernel accepted PeriodicGroup. con-leche itself first stopped at its recursion-fuel limit on a deep numeral recursion (task #348). After the reduction-order and fuel changes of task #353 (14 October), the journal records acceptance (2.2 GB).	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38019899278	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the PeriodicGroup solution (711 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-13	K. Kitamura (GitHub KitaKen1), Formal Conjectures issue #7284	Catalogue proposal	Proposes the statement that for every prime p there is an infinite finitely presented residually finite group in which every element has p-power order.	Open.
2026-10-13 to 2026-10-16	K. Kitamura, all-prime-residually-finite-p-groups (GitHub; proof commit c1ce611)	Extension (Lean; claimed)	Claims a Lean proof that for every prime p there is an infinite finitely presented residually finite p-group, a kernel G(p, n) in Stn over an infinite Fp-algebra for n ≥ 7. This implies the October result (p = 2) and the September theorem. The README states that 63 unchanged modules are reused from the openai/math repository and that the characteristic-p argument is new. It reports public Linux CI on Lean 4.34.1 (204 modules, Comparator acceptance of three statements, axiom audits with only the standard axioms, and a leanchecker --fresh replay). It includes a proof manuscript and an AI-usage disclosure (ChatGPT, OpenAI Codex, Claude Code).	Repository; the CI records are the author's.
2026-10-16	K. Kitamura, Formal Conjectures pull request #7412	Catalogue (formal statements)	Adds the finitely presented Burnside problem and two variants, residually finite periodic and residually finite p-groups for every prime p, each with a formal_proof link. According to the description, the main statement reuses the openai/math theorem and the variants are proved in the repository above.	Open, review required.

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.