Classifying spaces and geometric obstructions for Artin groups

3 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

Harmonic heights and the Artin K(pi,1) conjecture

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{Harmonic heights and the Artin $K(\pi,1)$ conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf}{OAI:Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026}},
  year = {2026}
}

An Artin group with no geometric CAT(0) action

OpenAI · 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.

Read PDF Download Source

Cite

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

Parabolic intersections in Artin groups

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Parabolic-intersections-in-Artin-groups-September-23-2026,
  author = {{OpenAI}},
  title = {{Parabolic Intersections in Artin Groups}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf}{OAI:Parabolic-intersections-in-Artin-groups-September-23-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 Artin \(K(\pi,1)\) conjecture asserts that the standard Salvetti complex of every finite-rank Artin group is aspherical. The formalized result proves the equivalent statement that its universal cover is contractible.

It applies to every Coxeter matrix on a finite generating set, including empty and disconnected diagrams and infinite edge labels. The associated Coxeter and Artin groups may be infinite. Later corollaries in the manuscript are not included.

The geometric-action question asks whether every Artin group acts properly and cocompactly by isometries on a proper CAT(0) space. The formalized result gives a counterexample: an Artin group defined by a symmetric matrix on \(116\) generators, with diagonal entries \(1\) and off-diagonal entries in \(\{2,3,\infty\}\).

It admits no such action on any nonempty proper CAT(0) space, in any dimension.

The formalization proves that the intersection of any family of parabolic subgroups of a finite-rank Artin group is parabolic. Every such intersection is already the intersection of at most the rank many members, and every subset has a unique parabolic closure. Both finite and infinite Coxeter labels are allowed.

For irreducible Artin groups with an infinite Coxeter label, it also proves acylindrical hyperbolicity and weak malnormality of every proper parabolic subgroup. These are the intersection and structural consequences selected from the paper.

Comparator links

Result	Comparator statement
Contractibility of the Salvetti cover	HarmonicArtin.lean
Artin group with no geometric \(\mathrm{CAT}(0)\) action	ArtinCAT0.lean
Parabolic intersections, closures, and structural consequences	ArtinParabolicIntersections.lean

Scope note on GitHub →