OAI.UniversalFInfinity.universal_group_of_type_FInfinity

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that, in a fixed universe, there exists a group H with the property HasTypeFInfinity, and every finitely presented group G in that same universe admits an injective group homomorphism G → H. Here HasTypeFInfinity(H) means there is a Hausdorff, connected topological space X carrying a CW complex structure on all of X with finitely many cells in each dimension n, such that for some basepoint x the fundamental group of X at x is isomorphic to H, and there exist a contractible topological space E and a surjective covering map p : E → X. So H is a universal group of this type, containing an isomorphic copy of every finitely presented group. The statement is admitted without proof.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/UniversalFInfinity.lean; bytes 497..745
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_UniversalFInfinity

namespace OAI

namespace UniversalFInfinity

universe u

Formal statement

theorem universal_group_of_type_FInfinity :
    ∃ (H : Type u) (groupH : Group H),
      @HasTypeFInfinity H groupH ∧
      ∀ (G : Type u) [Group G] [Group.IsFinitelyPresented G],
        ∃ φ : G →* H, Function.Injective φ := by
  sorry

end UniversalFInfinity
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/UniversalFInfinity.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by wurtle · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph