K(pi,1) conjecture for Artin groups

K(pi,1) conjecture for Artin groups

OpenAI's claim

OpenAI presents a proof in the selected manuscript. Every finite-rank Artin Salvetti complex is claimed aspherical, allowing arbitrary Coxeter labels.

Mathematical statement of the claimed result

Result 1.

Choose an arbitrary Coxeter matrix $M$ on a finite set $S$, allowing infinite labels. Let $W$ be its Coxeter group and $X(W,S)$ the Artin Salvetti complex, with a $|T|$-cell for each spherical subset $T\subseteq S$. The source claims \[ \widetilde{X(W,S)}\text{ contractible},\qquad \pi_n(X(W,S))=0\quad\text{for all }n\ge2. \] No connectedness condition is imposed on the Coxeter diagram.

Outline of the argument

A framed category records spherical parabolic cosets and the Artin action. Weighted harmonic heights and two-point estimates organize convex layers; cohomological tests on those layers remove the higher homotopy obstruction and establish the classifying-space property.

Formal verification

For family 254, the scope includes finite-rank Salvetti contractibility, the 116-generator Artin CAT$0$ counterexample, and arbitrary parabolic intersections with closure consequences. Each has its own Comparator statement. The listed Comparator files are ArtinCAT0.lean, ArtinParabolicIntersections.lean, HarmonicArtin.lean. Named declarations include OAI.ArtinCAT0.main, OAI.HarmonicArtin.salvetti_cover_contractible. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

• OpenAI, Harmonic heights and the Artin K($\pi$,1) conjecture, 2026-09-23; citation key OAI:Harmonic-heights-and-the-Artin-K-pi-1-conjecture-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 254: Lean scope.
• Comparator ArtinCAT0.json.
• Comparator ArtinCAT0.lean.
• Comparator ArtinParabolicIntersections.json.
• Comparator ArtinParabolicIntersections.lean.
• Comparator HarmonicArtin.json.
• Comparator HarmonicArtin.lean.
• OpenAI catalogue entry.

K(pi,1) conjecture for Artin groups

Definitions and mathematical statement

A finite Coxeter matrix $(m_{st})$ specifies the Artin group with generators $s\in S$ and relations equating the two alternating words of length $m_{st}$ when $m_{st}<\infty$; the Coxeter group also imposes $s^2=1$. A subset $T\subseteq S$ is spherical if its parabolic Coxeter group $W_T$ is finite. The quotient Salvetti complex has a $|T|$-cell for each spherical $T$, with the source's standard attaching maps. The target is \[ \pi_i(X_{W,S})=0\quad(i\ge2),\qquad\pi_1(X_{W,S})=A_{W,S}. \] Equivalently the source's Deligne complex of spherical-parabolic cosets is contractible. Attaching maps, not just cell counts, determine the complex. Arbitrary Coxeter labels are allowed; an unrestricted arrangement complement must not replace the Tits-cone model in infinite type.

Formulation and concept references: [S1].

Short English statement

Is the standard Salvetti space for every finite-generator Artin group aspherical, so that it is a classifying space for that group?

Research attempt: a complete right-angled subcase via vertex links

Status. We establish the target for all right-angled Artin groups, using the standard cubical nonpositive-curvature theorem as an explicit external input. The construction is the canonical Salvetti complex in this subcase. The resulting theorem is classical, as recorded in the primary survey [R1]; no novelty or solution for general Artin labels is claimed.

1. Identifying the spherical cells

Assume every off-diagonal label is either $2$ or $\infty$. Form the graph $\Gamma$ on $S$ with edges for label $2$. A subset $T$ whose vertices form a clique has parabolic Coxeter group $(\mathbb Z/2)^{|T|}$, hence is spherical. If $T$ contains two nonadjacent vertices, its Coxeter group maps onto the infinite dihedral group by retaining those two involutions and sending the others to the identity. This respects every commuting relation, so that parabolic cannot be finite. Therefore spherical subsets are exactly cliques.

The Salvetti space is consequently the union, inside the coordinate torus $(S^1)^S$, of the coordinate subtori corresponding to cliques, with the unused coordinates at a fixed basepoint. Its one-skeleton is a bouquet of circles. Each edge of $\Gamma$ gives a square with commutator attaching map; higher clique tori add the prescribed cubes. Thus its fundamental group has exactly the right-angled Artin presentation. Cells of dimension at least three do not change that group.

2. The flag-link calculation

There is one cubical vertex. The vertices of its link are the signed directions $s^+,s^-$ for $s\in S$. A set of signed directions spans a simplex precisely when it contains no opposite pair for one generator and its underlying generators form a clique in $\Gamma$.

Now take a set of link vertices that are pairwise adjacent. Opposite signs for the same generator are never adjacent, so the labels are distinct. Adjacency of two other directions means the two generator labels commute, hence all underlying labels form a clique. The corresponding coordinate cube supplies a simplex with exactly the chosen signs. Therefore every clique in the link spans a simplex: the link is flag.

The external cubical link criterion states that a finite-dimensional cube complex with flag vertex links is locally CAT$0$. Applying its universal-cover/Cartan--Hadamard conclusion gives a CAT$0$ universal cover. A CAT$0$ space is contractible by the continuous geodesic contraction to a basepoint. Hence all higher homotopy groups of this Salvetti complex vanish. Combined with the fundamental-group calculation, this proves it is a $K(A_\Gamma,1)$.

3. Direct checks at the two extremes

When $\Gamma$ has no edges, the complex is a bouquet of $|S|$ circles and its universal cover is the tree of reduced words. Removing the last letter gives the unique path toward the identity, which verifies the tree structure directly. When $\Gamma$ is complete, the complex is the full torus $(S^1)^{|S|}$, with universal cover $\mathbb R^{|S|}$. Both agree with the general link proof. The diagnostic enumerates all graphs on up to five vertices and verifies that every clique in the signed link is contained in one of the prescribed cube simplices; this is a finite check of the combinatorial implementation, not the proof for all graphs.

4. Why this does not extend by changing the labels

For a label $m_{st}>2$, the relation is an alternating braid word of length $m_{st}$ rather than a commutator square. The coordinate-torus construction then has the wrong attaching map. A finite Coxeter parabolic can also contain such labels, so the spherical-subset criterion used above is no longer "clique in a commuting graph." Merely retaining the same cell counts or drawing square cells would change the target space.

The source [S1] addresses other Artin settings; one must preserve its actual attaching maps and Tits-cone conventions. We have supplied no nonpositive-curvature metric or contraction for arbitrary labels. The unproved step is contractibility of the corresponding general universal cover or Deligne complex, not any remaining step in the right-angled calculation.

Sources

• S1 G. Paolini, The K(pi,1) conjecture for Artin groups of spherical type, arXiv:2607.24659v1 $2026$; R. Boyd, arXiv:2601.08658v1, Section 2.21. https://arxiv.org/html/2607.24659v1. Formulation source.
• R1 Ruth Charney, An introduction to right-angled Artin groups, especially the Salvetti complex and its CAT$0$ universal cover. https://arxiv.org/abs/math/0610668.