Group theory
14 families · 12 verified by lean
This page gathers the 14 result families that the openai/math repository catalogues under Group theory. Each claim comes from a manuscript; 12 of them have a Lean formalization checked by software, and the other 2 are still to be verified. Open any card to read a plain-language explainer, the original statement and its sources.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.