Subjects

Group theory

14 results from OpenAI’s math release. 14 explained so far. OpenAI has published Lean proofs for 12: 10 of the main theorem, 2 of part of the claim.

See these in the full list, with search and filters.

• 246 Cannon's conjecture

  Every word-hyperbolic group with boundary homeomorphic to S² 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.

  ▶Episode, 4:42 OpenAI published a Lean proof of the main theorem.

• 247 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 𝔽₂-algebra and a finitely presented infinite-dimensional algebraic unitization, giving negative answers to the corresponding nilpotence and Kurosh finiteness questions.

  2 papers ▶Episode, 4:48 OpenAI published a Lean proof of part of the claim.

• 248 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.

  ▶Episode, 4:46 OpenAI published a Lean proof of the main theorem.

• 249 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.

  ▶Episode, 4:34 OpenAI published a Lean proof of the main theorem.

• 250 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.

  3 papers ▶Episode, 4:46 OpenAI published a Lean proof of the main theorem.

• 251 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.

  2 papers ▶Episode, 4:36 OpenAI published a Lean proof of the main theorem.

• 252 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.

  ▶Episode, 5:08 OpenAI published a Lean proof of the main theorem.

• 253 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.

  ▶Episode, 4:13 OpenAI published a Lean proof of the main theorem.

• 254 Classifying spaces and geometric obstructions for Artin groups

  The Salvetti complex of every finite-rank Artin group is aspherical, proving the Artin $K(\pi,1)$ 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$(0)$ space.

  3 papers ▶Episode, 5:00 OpenAI published a Lean proof of the main theorem.

• 255 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.

  ▶Episode, 5:02 OpenAI published a Lean proof of the main theorem.

• 256 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.

  2 papers ▶Episode, 5:16 OpenAI published a Lean proof of part of the claim.

• 257 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 $\mathop{\mathrm{CAT}}\nolimits (0)$ space, in any dimension.

  ▶Episode, 4:25 OpenAI published a Lean proof of the main theorem.

• 258 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 $\mathrm{BS}(m,n)$, with $m,n\ne0$, is word-hyperbolic. It also proves that every word-hyperbolic one-relator group is virtually compact special.

  2 papers ▶Episode, 4:05

• 259 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.

  ▶Episode, 3:42

Summary and paper titles from OpenAI’s catalog, used under the Apache License 2.0. Last checked October 19, 2026.