Finitely presented Burnside problem answered negatively? (OpenAI, Lean)

Your AI and this story

Key facts

• Manuscript 1 (abstract, verbatim): ‘We construct an infinite group with an ordinary finite presentation in which every element has finite order, answering the finitely presented Burnside question negatively. We also construct an infinite-dimensional finitely presented nonunital nil associative algebra over F₂ that is Jacobson radical but not nilpotent.’ Theorem 1.1: ‘the construction below gives a unital associative F₂-algebra R for which St₁₂(R) is infinite, finitely presented, and periodic.’ Corollary 1.2: the group has Kazhdan’s property (T), hence is nonamenable (via Ershov and Jaikin-Zapirain’s theorem on Steinberg groups). 48 pages, dated 23 Sept 2026
• Manuscript 2 (5 Oct 2026, 25 pages): ‘We prove that the infinite, ordinarily finitely presented periodic Steinberg group Γ = St₁₂(R) of a companion paper is residually finite. Its finite-index subgroup G = ker(Γ → St₁₂(F₂)) is infinite, ordinarily finitely presented, and residually finite, and every element of G has finite 2-power order. The orders of its elements are unbounded’
• Background as the paper recounts it: Burnside’s questions started the study of finiteness under restrictions on element orders; Golod built infinite finitely generated periodic groups from nil algebras via the Golod–Shafarevich inequality; Novikov and Adian built infinite finitely generated groups of bounded exponent; Zelmanov solved the restricted Burnside problem; Ol’shanskii and Sapir ‘explicitly distinguish the finitely presented periodic-group question’. Infinite finitely generated periodic groups with property (T) were known (Ershov); the new claim is the combination with an ordinary finite presentation
• Lean (OpenAI scope note lean/docs/247.md): ‘The formalization gives a negative answer by constructing an infinite finitely presented periodic group, including a witness realized as a Steinberg group over an algebra of characteristic two. Periodicity means that each element has some finite order; no common exponent is asserted. The paper’s separate nil-algebra and radical-algebra conclusions are outside these selected statements.’ Challenge PeriodicGroup: ‘accepted’ in the oai-math-revised comparator run of 25–26 Oct. The residually finite 2-group is not in the scope note
• Follow-up: Kenta Kitamura’s GitHub repository claims infinite finitely presented residually finite p-groups for every prime p, with a Lean proof; its README opens ‘OpenAI solved the following finitely presented Burnside problem’. His formal-conjectures PR #7412 (opened 16 Oct, still open) would add the problem with ‘research solved’ tags, reusing OpenAI’s theorem for the main statement
• Reactions: none from group theorists on this paper found (web, Hacker News, oai-math-revised notes) as of 29 Oct. In general reactions, Xiaolei Wu wrote that the release’s group-theory section ‘looked unreal. These were almost all the major open problems in my field!’ (Proofs and Prompts, 8 Oct)