Oct 6, 2026
Lean formalization in OpenAI math repository (Result 253)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An infinite finitely presented simple amenable group'. We construct an infinite finitely presented simple amenable group, giving a positive answer to the finite-presentation existence question for simple amenable groups.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 253). The Lean development was not rebuilt locally.