# Classifying spaces and geometric obstructions for Artin groups

> Proves the Artin K(π,1) conjecture in finite rank, and finds an Artin group with no geometric CAT(0) action.

Canonical: https://closedform.nishachay.tech/e/openai-math-2026-254/
Last updated: 2026-10-14

**Proves the Artin K(π,1) conjecture in finite rank, and finds an Artin group with no geometric CAT(0) action.**

**Trust:** Formal proof listed · **Papers:** 3 · **First paper:** September 23, 2026 · **Field:** Group theory · **Entry:** 254

*Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error.

Artin groups are built from generators and braid-like rules, like the groups that describe tangled strings. A decades-old conjecture says a standard space built from these rules has no hidden higher holes. The first paper proves this for every Artin group with finitely many generators, with a Lean formalization listed. Two companion papers find an Artin group with no nice curved geometry and show that its special subgroups intersect well.

## At a glance

- **First step:** 1972 (Pierre Deligne, who proved the spherical case using finite real reflection arrangements)
- **Significance:** Major. The K(π,1) conjecture is a central open problem for Artin groups, and CAT(0) actions were widely expected.
- **Trust:** Formal proof listed
- **Field:** Group theory (3 papers)

## The explanation

Take two generators, a and b, with one rule: aba = bab. This is the braid group on three strands. Swap strands 1 and 2, then 2 and 3, then 1 and 2 again. You get the same braid as swapping 2 and 3, then 1 and 2, then 2 and 3. An Artin group allows such a rule for each pair of generators. A label m says both alternating words of length m are equal; the label ∞ imposes no rule[1]. Adding the rule that each generator squared is 1 gives the Coxeter group[1]. For a and b with label 3, the Coxeter group has 6 elements, like the symmetries of a triangle.

The Salvetti complex is a space with one cell of dimension |T| for each spherical subset T[2]. A subset is spherical when its Coxeter group is finite. For the braid example, the subsets ∅, {a}, {b} and {a, b} are all spherical. So the space has 1 point, 2 loops and 1 disc. Its Euler characteristic is 1 − 2 + 1 = 0. With label ∞ instead, {a, b} is not spherical. The space is two loops at a point, with Euler characteristic 1 − 2 = −1. The K(π,1) conjecture asks that this space be aspherical. That means its universal cover can shrink to a point, so all higher homotopy groups vanish.

Deligne proved the spherical case in 1972[3]. Charney and Davis covered FC type and dimension at most two[4]. Paolini and Salvetti covered affine types[5]. Huang and Przytycki covered dimension at most three[6]. The general case stayed open. The first paper proves it for every Coxeter matrix on a finite set[7]. Labels may be finite or infinite, and diagrams may be disconnected[7].

The second paper asks about geometry. A CAT(0) space is one whose triangles are at least as thin as flat ones. A geometric action is proper and cocompact on such a space. Haettel recorded the expectation that every finite-rank Artin group has one[8]. Brady and Crisp showed an obstruction in two dimensions can vanish in three[9]. So a counterexample must work in every dimension. The paper proves there is an Artin group on 116 generators, with labels in {2, 3, ∞}, that has no geometric action[10].

The third paper studies parabolic subgroups, which are conjugates of subgroups generated by some of the generators[11]. It proves that the intersection of any two parabolic subgroups is parabolic[12]. A corollary is that arbitrary intersections are parabolic, and every subset has a smallest parabolic subgroup containing it[13]. The paper also claims a decidable word problem for every finite-rank Artin group[14].

How sure is this? A computer proof checker called Lean has formal proofs of the contractible Salvetti cover, the 116-generator counterexample, and the parabolic intersection results. The Lean note leaves out later corollaries in the manuscripts. No specialist review of these papers has been published.

**What it doesn't show.** This does not cover Artin groups with infinitely many generators, and the Lean note leaves out the later corollaries in the manuscripts.

## Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

## Hype check

Major if it holds, and the three main theorems have Lean formalizations. Later corollaries are not in the Lean note. No specialist review is published.

## Words used

- **Artin group:** A group with generators and, for some pairs, a rule that two alternating words of a given length are equal.
- **Coxeter group:** The group obtained from an Artin group by adding the rule that each generator squared is the identity.
- **Spherical subset:** A set of generators whose Coxeter group is finite.
- **Salvetti complex:** A space built from cells, one for each spherical subset, whose loops form the Artin group.
- **Aspherical:** Having a universal cover that can be shrunk to a point, so there are no higher-dimensional holes.
- **CAT(0) space:** A space whose geodesic triangles are at least as thin as triangles in a flat plane.
- **Geometric action:** A proper, cocompact action by isometries on a nonempty proper CAT(0) space.
- **Parabolic subgroup:** A conjugate of a subgroup generated by some of the standard generators.

## The original papers (3)

- [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf) - September 23, 2026 · Formal proof listed
- [An Artin group with no geometric CAT(0) action](https://github.com/openai/math/blob/main/preprints/An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026/paper.pdf) - September 23, 2026 · Formal proof listed
- [Parabolic intersections in Artin groups](https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf) - September 23, 2026

- [Lean notes](https://github.com/openai/math/blob/main/lean/docs/254.md)

## Quoted lines from the paper (14)

[1] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> The Coxeter group \(W\) is the quotient obtained by imposing \(\sigma_s^2=1\).

[2] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> The standard Artin Salvetti complex \(X(W,S)\) has one cell of dimension \(|T|\) for each spherical subset \(T\), including its vertex for \(T=\varnothing\).

[3] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> Deligne proved the spherical case using finite real reflection arrangements.

[4] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> They proved the FC case, in which every subset with all pairwise labels finite is spherical, and the dimension-at-most-two case.

[5] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> Paolini--Salvetti resolved all affine types using dual noncrossing partitions and discrete Morse theory, building on the dual and Garside constructions of McCammond--Sulway.

[6] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> Huang--Przytycki proved the dimension-at-most-three case and additional specified higher-dimensional classes.

[7] From [Harmonic heights and the Artin K(pi,1) conjecture](https://github.com/openai/math/blob/main/preprints/Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026/paper.pdf):

> The conclusion allows arbitrary finite labels, infinite labels, and connected or disconnected diagrams.

[8] From [An Artin group with no geometric CAT(0) action](https://github.com/openai/math/blob/main/preprints/An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026/paper.pdf):

> The affirmative expectation that every finite-rank Artin group admits a geometric action is recorded by Haettel as Conjecture 1.1 of.

[9] From [An Artin group with no geometric CAT(0) action](https://github.com/openai/math/blob/main/preprints/An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026/paper.pdf):

> Their examples show that an obstruction in one dimension can disappear in a higher-dimensional CAT(0) space.

[10] From [An Artin group with no geometric CAT(0) action](https://github.com/openai/math/blob/main/preprints/An-Artin-group-with-no-geometric-CAT-0-action-September-23-2026/paper.pdf):

> There is an Artin matrix \(M\) on 116 generators, with every off-diagonal label in \(\{2,3,\infty\}\), such that \(A_M\) admits no geometric action.

[11] From [Parabolic intersections in Artin groups](https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf):

> A \emph{parabolic subgroup} is a conjugate of some $A_X$.

[12] From [Parabolic intersections in Artin groups](https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf):

> For every Coxeter matrix $M$ on a finite set $S$, subsets $X,Y\subseteq S$, and $g,h\in A_M$, there are $Z\subseteq S$ and $k\in A_M$ such that \[ gA_Xg^{-1}\cap hA_Yh^{-1}=kA_Zk^{-1}. \]

[13] From [Parabolic intersections in Artin groups](https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf):

> In particular, arbitrary intersections of parabolic subgroups are parabolic, and every subset $E\subseteq A$ is contained in a unique smallest parabolic subgroup.

[14] From [Parabolic intersections in Artin groups](https://github.com/openai/math/blob/main/preprints/Parabolic-intersections-in-Artin-groups-September-23-2026/paper.pdf):

> In particular, the word problem is decidable for every finite-rank Artin group.

## Other sources

- [openai/math, Lean scope note for family 254](https://github.com/openai/math/blob/main/lean/docs/254.md): “The formalized result proves the equivalent statement that its universal cover is contractible.”
- [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model”

## Related

- [Boone–Higman embeddings with higher finiteness](https://closedform.nishachay.tech/e/openai-math-2026-250/) - Group theory
- [Thompson's group F is nonamenable](https://closedform.nishachay.tech/e/openai-math-2026-248/) - Group theory
- [An infinite finitely presented simple amenable group](https://closedform.nishachay.tech/e/openai-math-2026-253/) - Group theory
- [Quasi-isometric recognition of virtually polycyclic groups](https://closedform.nishachay.tech/e/openai-math-2026-255/) - Group theory
- [A torsion-free hyperbolic group that is neither residually finite nor linear over any field](https://closedform.nishachay.tech/e/openai-math-2026-252/) - Group theory
- [Group theory](https://closedform.nishachay.tech/science/mathematics/group-theory/) - Field · 14 results
- [Open since the 1970s](https://closedform.nishachay.tech/open-since/1970s/) - Era · 63 results
- [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results
- [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20254%5D%20)