Browse › Group theory › 254 Classifying spaces and geometric obstructions for Artin groups
Harmonic heights and the Artin K(pi,1) conjecture
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
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.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Formalization
- OpenAI math release, Lean scope notes for family 254: Classifying spaces and geometric obstructions for Artin groups (lean/docs/254.md, undated). States that the formalized result is contractibility of the universal cover of the Salvetti complex for every finite-rank Coxeter matrix, including empty and disconnected diagrams and infinite labels, and that the manuscript's later corollaries are not included. [family-level]
- OpenAI math release, HarmonicArtin.lean comparator statement (lean/ComparatorChallenges). The comparator statement file for this paper's main theorem (
salvetti_cover_contractible), which the scope notes link as the Lean formulation of Theorem 1.1.
Possibly relevant literature (found by the agent, not checked)
- J. Huang, Cycles in spherical Deligne complexes and application to K(π,1)-conjecture for Artin groups (arXiv:2405.12068, 2024). Proves the conjecture for 3-dimensional hyperbolic-type Artin groups (with one exception) and for complete bipartite Coxeter diagrams; these are previously known classes not in the paper's survey of prior cases (Section 1.1), which cites other work of Huang.
- O. Garnier, E. Heng, A. Licata, O. Yacobi, Normalisers of parabolic subgroups of Artin–Tits groups and Tits cone intersections (arXiv:2509.21915, 2025). Proves K(π,1) results for Tits-cone-intersection arrangements in finite type, by authors of the Heng–Licata framework whose categorical construction the paper adapts.
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 254
Independent sites; their content is not reviewed here.
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}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/254.md. The Lean statements have not been checked by people against the paper's claims.
Family 254: Classifying spaces and geometric obstructions for Artin groups
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.
Other papers in this family:
- An Artin group with no geometric CAT(0) action · September 23, 2026
- Parabolic intersections in Artin groups · September 23, 2026