Infinite finitely presented simple amenable groups

Infinite finitely presented simple amenable groups are the subject of an existence question: can a group be infinite, finitely presented, simple and amenable at the same time? Infinite finitely generated simple amenable groups were known, but finite presentation remained open. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims an affirmative answer. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

• As recounted in the introduction of the manuscript:
  • Giordano, Putnam and Skau developed topological full groups as invariants of Cantor minimal systems. Matui proved that their derived groups are simple, characterized when they are finitely generated, and proved that the derived groups arising from minimal subshifts are not finitely presented.
  • Juschenko and Monod proved that the full group of every minimal homeomorphism of a Cantor space is amenable. Combined with the earlier structure theory, this gives infinite finitely generated simple amenable groups.
  • The question for finitely presented groups is recorded by Button (2010) and raised again by Juschenko and Monod. Grigorchuk and Medynets proved that these full groups are locally embeddable into finite groups, which explains why the classical examples cannot be finitely presented.
  • Later constructions include Nekrashevych's simple torsion groups of intermediate growth and two-generated infinite simple amenable groups of Kionke and Schesler; neither gives finite presentation. The manuscript cites Zaremsky's problem list (version of July 2026, Problem 10) for the question.

The original result

• Claim. Theorem thm:main of An infinite finitely presented simple amenable group states that there exists an infinite finitely presented simple amenable group.
• Method, as described: the group is an alternating subgroup of a group of piecewise translations of finitely many squares. The pieces are polygons whose edges lie on lines of four directions, at levels in the ring of integers of the golden-ratio field. The manuscript proves simplicity from strict area comparison, amenability from random polygonal partitions built from correlated random fields, finite generation of the Schur multiplier through homological stability, and a finitely presented central extension by propagating relations along inclined lines. A five-term exact sequence then gives finite presentation for one sufficiently large number of squares.
• Sources. At commit 1581d4c: An infinite finitely presented simple amenable group.
• Formalization, as described by the repository. The scope note states that the formalized result answers the existence question affirmatively, with amenability expressed by the Følner condition, and that later general claims about central kernels and enlargements across families are not included. The Comparator statement is SimpleAmenable.lean.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 24 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit 8e51ac0, 23 October 2026)	Review (fidelity of the formal statements)	Rates this family "full": the Lean statement is the existence of an infinite, finitely presented, simple group satisfying the Følner condition, which MathVet notes is a custom definition of amenability, equivalent for discrete groups but not Mathlib's notion. It records a sandboxed Comparator pass for the challenge SimpleAmenable (8 October 2026).	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-08	M. C. B. Zaremsky, Some open problems, problem list on the author's website, version dated 8 October 2026	Remark	Problem 1.10 of the list, "Find a finitely presented (or F∞), infinite, simple, amenable group", is crossed out. A note added to the list on 8 October 2026 reads "I'll just cross out problems solved by AI". Problem 1.12, "Find an amenable, non-elementary amenable group of type F∞", is not crossed out.	The list does not name the work that solved each crossed-out problem.
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 SimpleAmenable solution (2,078 s).	Repository.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list SimpleAmenable, so the challenge was accepted by con-leche and by Lean's official kernel.	Development journal.

Notes

• The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.