An infinite finitely presented simple amenable group

Comments and discussion

• Matthew C. B. Zaremsky, Some open problems (author's problem list, version dated October 8, 2026). The paper cites the July 12, 2026 version (Problem 10, "Find a finitely presented (or F∞), infinite, simple, amenable group."); in the October 8 version this problem is struck through with the note "Update 10/8/26: I'll just cross out problems solved by AI." [cites earlier version]

Formalization

• OpenAI math release, Lean scope notes for family 253 (lean/docs/253.md, 2026-10-06). The release's scope note: the Lean result is the bare existence statement, with amenability in Følner form; the paper's later general claims about central kernels and enlargements across families are not covered.
• OpenAI, lean/OAI/GroupTheory/SimpleAmenable/Main.lean (github.com/openai/math, commit adc7f12). Lean theorem main asserting that some group satisfies Infinite G ∧ Group.IsFinitelyPresented G ∧ IsSimpleGroup G ∧ FolnerAmenable G.

Possibly relevant literature (found by the agent, not checked)

• Mustafa Gökhan Benli, Rostislav Grigorchuk and Pierre de la Harpe, Amenable groups without finitely presented amenable covers (Bulletin of Mathematical Sciences 3, 73–131, 2013). Studies obstructions to amenable finitely presented covers, including Problem 1.12 for the Juschenko–Monod simple amenable groups, which is background for the paper's finitely presented central cover of its polygon exchange group.
• Kate Juschenko, Volodymyr Nekrashevych, Mikael de la Salle, Extensions of amenable groups by recurrent groupoids (arXiv:1305.2637; Invent. Math. 206 (2016)). A general amenability criterion based on recurrent orbital Schreier graphs covering full groups of Cantor minimal systems, relevant to the paper's comparison of its amenability argument with the Juschenko–Monod and extensive-amenability methods.
• Hiroki Matui, Topological full groups of one-sided shifts of finite type (arXiv:1210.5800, 2012). Shows that full groups of one-sided irreducible shifts of finite type are of type F∞ with simple commutator subgroups, contrasting with the minimal-subshift case the paper discusses via Matui 2006.
• Volodymyr Nekrashevych, Finitely presented groups associated with expanding maps (arXiv:1312.5654, 2013). Constructs finitely presented groups of dynamical origin with simple commutator subgroups, relevant to the paper's strategy for obtaining finite presentation for full-group-type groups.