Hyperbolic groups without geometric CAT(0) actions
From OpenAI Aftermath
Hyperbolic groups without geometric CAT(0) actions concerns the question whether every word-hyperbolic group acts properly and cocompactly by isometries on a proper CAT(0) space, or on a proper CAT(−1) space. A manuscript in OpenAI's public mathematics collection, dated 25 September 2026, claims a hyperbolic group with a finite two-dimensional classifying space that has no such action on any proper complete CAT(0) space, in any dimension. The collection's Lean formalization covers the main statement without two of its clauses.
Background
- As recounted in the manuscript's introduction:
- The realization question. A linear isoperimetric inequality characterizes word-hyperbolicity for finitely presented groups, while CAT(0) and CAT(−1) comparison is a local form of nonpositive and negative curvature. Gromov recalls spending years seeking geometric realizations of hyperbolic groups by negatively curved spaces. The CAT(−1) question is Problem H11 of the 1999 problem list of Baumslag, Myasnikov and Shpilrain, and both questions appear as open problems in Stark's 2025 survey and in a March 2026 preprint of Duchesne and Simon.
- Positive cases. Free groups act on trees and closed hyperbolic manifold groups act on hyperbolic space; finite complexes with locally CAT(0) or CAT(−1) metrics give geometric actions on their universal covers; and Ollivier and Wise proved that random groups at density below 1/6 act freely and cocompactly on CAT(0) cube complexes.
- Earlier obstructions. Brady and Crisp constructed torsion-free hyperbolic groups of geometric dimension two with no proper isometric action on a proper two-dimensional CAT(0) space, and a hyperbolic group of CAT(0) dimension two and CAT(−1) dimension three. These obstructions use translation lengths in two-dimensional targets.
- Fixed-point methods. The obstruction uses the harmonic-energy framework of Gromov and of Izeki and Nayatani, in which expansion forces fixed points for targets with a suitable nonlinear spectral inequality; earlier results of Izeki, Kondo and Nayatani and of Toyoda give such bounds only for prescribed target classes.
The original result
- Claim, 25 September 2026. The main theorem of A hyperbolic group with no geometric CAT(0) action states that there are a finite connected two-dimensional aspherical simplicial complex K and a constant C such that every edge loop of length ℓ in the universal cover of K bounds a disk diagram with at most Cℓ triangles, and the group π1K admits no proper cocompact isometric action on a proper complete CAT(0) space. Hence π1K is word-hyperbolic, and no finite simplicial complex homotopy equivalent to K admits a compatible locally CAT(0) or locally CAT(−1) geodesic length metric.
- Scope, as stated: the proof is an existence argument and gives no effective size for K; the filling constant may depend on the selected finite presentation.
- Method, as described: random finite presentations follow a template built on the Fano plane; a counting argument for disk diagrams, with repeated relator occurrences charged once, gives hyperbolicity and asphericity with high probability. A hypothetical geometric CAT(0) action, chosen after the presentation, is excluded by a harmonic-energy argument made uniform through displacement bounds, couplings of table matches and Sturm's inductive means.
- Sources. Commit
adc7f12of the openai/math repository: A hyperbolic group with no geometric CAT(0) action. - Formalization. The scope note states that the Lean development constructs a finite connected aspherical complex with a linear disk-filling bound whose word-hyperbolic fundamental group admits no geometric action on a nonempty proper complete CAT(0) space, and excludes locally CAT(−1) geodesic metrics on every finite complex homotopy equivalent to it. It states that the two-dimensionality of the witness and the exclusion of locally CAT(0) models are not included. Comparator statement:
HyperbolicObstruction.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 31 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet, a GitHub review of openai/math, tables at repository commit c76f1e4 of 14 October 2026 |
Review, fidelity of the formal statements | Rates this family "full": the challenge states a finite aspherical complex with word-hyperbolic fundamental group, a linear disk-filling bound, no geometric action on any nonempty proper complete CAT(0) space and no compatible locally CAT(−1) metric on homotopy-equivalent complexes, matching the summary. It lists the hand-written definitions of CAT(0) spaces, word-hyperbolicity and finite complexes as definitions to check, and records a sandboxed Comparator pass on 8 October 2026. | Review repository. Read on 31 October 2026. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38051470892 | Verification, two kernels | Records the challenge HyperbolicObstruction as certified: Lean's default kernel and the nanoda kernel both accept the solution, in 1,356 s. C. Toledo's report lists the lane's results. |
Repository. The run concerns the formalized statement only. |
| 2026-10-10 to 2026-10-14 | con-leche development journal, task #348 | Verification, second kernel | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list this family's challenge, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-14 to 2026-10-16 | M. Lupini, Robust fixed points and finite classifying spaces: CAT(0) actions, Banach targets and group fillings, preprint, Zenodo 10.5281/zenodo.23424960, version of 16 October 2026 | Uses, extension | From this manuscript's group construction, diagram argument and analytic obstruction, the preprint obtains infinite torsion-free hyperbolic groups with finite two-dimensional classifying spaces whose isometric actions on every nonempty complete CAT(0) space have a fixed point, which it says answers an existence question recorded by Eskenazis, Mendel and Naor in 2019; it states that the qualitative conclusion can also be extracted from the manuscript's analytic argument by standard uniformization. It also characterizes the CAT(0) fixed-point property of a finitely presented group by finite systems of polynomial distance inequalities. | Preprint on Zenodo, first version 14 October 2026, with its LaTeX source and exact-check scripts. No outside review was found. |
| 2026-10-17 | AI Proved What?, episode 257 Hyperbolic, but never CAT(0)? An answer to Gromov's question, remade version of 22 October 2026 | Reading, exposition | Video explainer of the 43-page preprint. It recalls Gromov's description of the realization question as foundational, the two-dimensional obstructions of Brady and Crisp in 2007, and the Duchesne–Simon preprint of 2026, and illustrates the Fano-plane template and the forced cube geometry in the proof. It states that the preprint gives no explicit group or size, and claims nothing about Gromov's random groups, actions that are not cocompact or spaces that are not proper. | Episode status, last checked 30 October 2026: posted as a preprint, not revised; under expert review, not yet; peer reviewed, not yet; checked in Lean, the main statement with two clauses left out, about 57,000 lines that the site did not build; no specialist comment found. The site states that it is made with Anthropic's Claude. Read on 31 October 2026. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
- A related manuscript of the collection on non-residually-finite hyperbolic groups is described on Residual finiteness of hyperbolic groups, whose follow-up list also includes the Lupini preprint.
