Group theory
14 results in OpenAI Math 2026.
14 AI-made results in group theory, from 22 papers in the OpenAI math collection, each explained in plain English. 12 have a formal Lean proof listed; 2 are claimed in a paper and not yet machine-checked. The oldest question here dates back to 1902: An infinite finitely presented residually finite 2-group and a finitely presented nil algebra.
Group theory14
-
Cannon's conjecture
Every word-hyperbolic group with boundary homeomorphic to S2 admits a proper cocompact isometric action on hyperbolic three-space with finite kernel, proving Cannon's conjecture. Every torsion-free such group is therefore the fundamental group of a closed hyperbolic three-manifold.
Formal proof listed -
An infinite finitely presented residually finite 2-group and a finitely presented nil algebra
Constructs an infinite finitely presented residually finite group whose elements all have finite 2-power order, answering the finitely presented Burnside problem negatively even in this class. The construction also yields an infinite-dimensional finitely presented nil associative 𝔽2-algebra and a finitely presented infinite-dimensional algebraic unitization, giving negative answers to the corresponding nilpotence and Kurosh finiteness questions.
Formal proof listed -
Thompson's group F is nonamenable
Proves that Thompson's group F, the group of dyadic piecewise linear homeomorphisms of the interval, is nonamenable, resolving its longstanding amenability problem.
Formal proof listed -
A finitely generated Eilenberg–Ganea counterexample
Constructs a finitely generated residually finite group with integral cohomological dimension two and geometric dimension three, disproving the Eilenberg–Ganea conjecture. It has no two-dimensional classifying space, even with infinitely many cells.
Formal proof listed -
Boone–Higman embeddings with higher finiteness
A finitely generated group has decidable word problem exactly when it embeds in a finitely presented simple group, proving the Boone–Higman conjecture. The target can have type F∞: a classifying space with finitely many cells in each dimension. A single group of type F∞ can also contain every finitely presented group.
Formal proof listed -
Amenability, unitarizability, and strong Ulam stability
Resolves Dixmier's problem for all discrete groups: amenability is equivalent to every uniformly bounded Hilbert-space representation being similar to a unitary representation. For countable discrete groups, amenability is also equivalent to strong Ulam stability: sufficiently accurate unitary approximate representations are uniformly close in operator norm to genuine representations on the same, possibly infinite-dimensional, Hilbert space.
Formal proof listed -
A torsion-free hyperbolic group that is neither residually finite nor linear over any field
Constructs a torsion-free word-hyperbolic group that is not residually finite, answering the residual-finiteness question negatively. One fixed nonidentity element is killed by every finite-dimensional linear representation over every commutative field, so the group is not linear over any such field.
Formal proof listed -
An infinite finitely presented simple amenable group
Constructs an infinite finitely presented simple amenable group, answering the longstanding question of whether these properties can occur simultaneously.
Formal proof listed -
Classifying spaces and geometric obstructions for Artin groups
The Salvetti complex of every finite-rank Artin group is aspherical, proving the Artin conjecture. Arbitrary intersections of its parabolic subgroups are parabolic, proving the Parabolic Intersection Conjecture. An explicit Artin group admits no proper cocompact isometric action on any nonempty proper CAT space.
Formal proof listed -
Quasi-isometric recognition of virtually polycyclic groups
Proves that every finitely generated group quasi-isometric to a finitely generated virtually polycyclic group is virtually polycyclic, resolving the Eskin–Fisher–Whyte lattice-recognition conjecture. Equivalently, a group quasi-isometric to a lattice in a connected simply connected solvable Lie group is virtually a uniform lattice in some such Lie group, possibly a different one.
Formal proof listed -
Nonsingular systems of equations over arbitrary groups
Proves that every finite system of equations over an arbitrary group whose exponent-sum matrix has full row rank over ℚ has a simultaneous solution in an overgroup, resolving Howie's conjecture. The coefficient group embeds in the presented quotient. A companion proves Kervaire's conjecture: adjoining one generator and one relation cannot trivialize a nontrivial group.
Formal proof listed -
A hyperbolic group without a geometric CAT(0) action
Answers negatively whether every word-hyperbolic group is a CAT(0) group. Constructs one with a finite classifying space but no proper cocompact isometric action on any proper complete space, in any dimension.
Formal proof listed -
Gersten’s conjecture and virtual compact specialness of one-relator groups
Proves Gersten's conjecture: every finitely generated one-relator group containing no Baumslag–Solitar subgroup , with , is word-hyperbolic. It also proves that every word-hyperbolic one-relator group is virtually compact special.
Claimed, not checked -
A group without fixed price
Constructs a finitely generated group with two essentially free probability-measure-preserving actions of different costs, answering the general fixed-price problem negatively. Its Bernoulli action has cost bounded away from one, while a sequence of finite height extensions has costs tending to one.
Claimed, not checked