Whitehead asphericity conjecture

### What is the conjecture

A CW complex is aspherical if all its homotopy groups are trivial, i.e., $\pi_n(X) = 0$ for all $n \geq 1$. The Whitehead asphericity conjecture states that every connected subcomplex of a two-dimensional aspherical CW complex is itself aspherical. Equivalently, for any aspherical 2-dimensional group presentation, every sub-presentation obtained by removing some relations remains aspherical.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://en.wikipedia.org/wiki/Whitehead_conjecture, https://arxiv.org/abs/1308.4441, https://projecteuclid.org/journals/illinois-journal-of-mathematics/volume-43/issue-4/Some-remarks-on-the-Whitehead-asphericity-conjecture/10.1215/ijm/1256060692.full

### Prerequisites needed

**Formalizability Rating:** 4/5 (0 is best) (as of 2026-02-06)

Building blocks (from search results):
- CW complexes and cellular homology (general topology concepts)
- Homotopy groups and fundamental group structure
- Group presentations and relations

Missing pieces:
- Formalization of aspherical spaces and asphericity as a property in Lean (no Mathlib definitions found for aspherical in the context of CW complexes)
- Infrastructure for group presentations with generators/relations and their topological interpretation via CW complexes

Rating justification: While basic homotopy group theory exists in Mathlib, the notion of aspherical spaces and the relationship between group presentations and their geometric realizations as CW complexes requires substantial new definitions and theory. Stating the conjecture would need a proper formalization of aspherical CW complexes and sub-presentations.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-55
* ams-20
* ams-57

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)