Oct 6, 2026
Lean formalization in OpenAI math repository (Result 250)
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 'A universal group of type F∞'. We construct a single group of type F∞ containing every finitely presented group. Its finitely generated subgroups, up to isomorphism, are exactly the finitely generated recursively presented groups. This answers the F∞ form of the higher-dimensional Higman embedding question.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 250). The Lean development was not rebuilt locally.