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. (Lean)
Manuscripts (3)
Harmonic heights and the Artin K(pi,1) conjecture
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026}
We prove that the standard Salvetti complex of every Artin group with finitely many standard generators is aspherical. This resolves the Artin K(\pi,1) conjecture in finite rank.
An Artin group with no geometric CAT(0) action
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026}
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.
Parabolic intersections in Artin groups
September 23, 2026 · source · cite as \cite{OAI:Parabolic-intersections-in-Artin-groups-September-23-2026}
We prove that every intersection of parabolic subgroups of any finite-rank Artin group, with arbitrary finite or infinite Coxeter labels, is parabolic. This resolves the Parabolic Intersection Conjecture affirmatively.
Result 254 · Group theory. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md