Oct 6, 2026
Lean formalization in OpenAI math repository (Result 257)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A hyperbolic group with no geometric CAT(0) action'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 257). The Lean development was not rebuilt locally.