AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

An Artin group with no geometric CAT(0) action

Can the mathematical statement in An Artin group with no geometric CAT(0) action be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 254)

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 'An Artin group with no geometric CAT(0) action'. We construct an Artin group on 116 generators that admits no proper, cocompact isometric action on a nonempty proper CAT(0) space. This refutes the CAT(0) conjecture for Artin groups.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 254). The Lean development was not rebuilt locally.