AI Proof WatchKeep up with AI contributions

Universal groups of type F∞

Is there a group of type F∞ containing every finitely presented group? Type F∞ means it admits a classifying space with finite skeleta in every dimension.

Why it matters and what counts as progress

Why it matters: The finiteness condition would strengthen Higman’s universal finitely presented embedding construction.

What counts as progress: A universal containing group with all finite-skeleton properties proved, including the asserted classification of its finitely generated subgroups, or an obstruction to such universality.

How the problem developed

  1. 1961 · Embedding theorem [1]

    Graham Higman Proved that every finitely generated recursively presented group embeds in a finitely presented group.

  2. 19 Oct 2016 · Embedding theorem [2]

    Ian Leary Circulated a construction embedding every countable group in a group of type FP₂.

  3. 23 Sept 2026 · Reported claim [3]

    OpenAI Reported one group of type F∞ containing an embedded copy of every finitely presented group.

AI contribution

Sources

  1. Higman, Subgroups of finitely presented groups
  2. Leary, Subgroups of almost finitely presented groups
  3. OpenAI universal F∞ group manuscript
  4. A universal group of type F∞
  5. Lean universal-group development
  6. Lean formalization scope
Website timeline

Publication dates and editorial changes.