∑math20

Group theory · Result 257

A hyperbolic group without a geometric CAT(0) action

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of A hyperbolic group with no geometric CAT(0) action

A hyperbolic group with no geometric CAT(0) action

OpenAI · September 25, 2026

We construct a hyperbolic group with a finite classifying space that admits no geometric action on a proper complete CAT(0) space. Consequently, a finite aspherical simplicial complex with a linear combinatorial disk-filling inequality need not have a finite locally CAT(0) homotopy model, and hence need not have a finite locally CAT(−1) model. Here metric models carry geodesic length metrics inducing the given complex topology.

Read PDF Download Source

Cite
@misc{OAI:A-hyperbolic-group-with-no-geometric-CAT0-action-September-25-2026,
  author = {{OpenAI}},
  title = {{A hyperbolic group with no geometric CAT(0) action}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-hyperbolic-group-with-no-geometric-CAT0-action-September-25-2026/paper.pdf}{OAI:A-hyperbolic-group-with-no-geometric-CAT0-action-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result constructs a finite connected aspherical complex with a linear disk-filling bound whose fundamental group is word-hyperbolic but admits no geometric action on a nonempty proper complete \(\mathrm{CAT}(0)\) space. It also excludes locally \(\mathrm{CAT}(-1)\) geodesic metrics on every finite complex homotopy equivalent to the witness. The stronger claims that the witness is two-dimensional and that those models admit no locally \(\mathrm{CAT}(0)\) metric are not included.

Comparator links

ResultComparator statement
Hyperbolic group with no geometric CAT(0) actionHyperbolicObstruction.lean

Scope note on GitHub →