Eilenberg-Ganea Conjecture

### What is the conjecture

If a group $G$ has cohomological dimension 2, then it has a 2-dimensional Eilenberg–MacLane space $K(G,1)$. Equivalently, there exists a 2-dimensional aspherical CW complex $X$ with fundamental group $\pi_1(X) = G$.

**Sources:**
- https://en.wikipedia.org/wiki/Eilenberg–Ganea_conjecture, https://en.wikipedia.org/wiki/Eilenberg–Ganea_theorem, https://ems.press/content/serial-article-files/30147

### Prerequisites needed

**Formalizability Rating:** 4/5 (as of 2026-01-20)

The conjecture requires formalization of significant algebraic topology infrastructure not yet present in Mathlib. Key missing components include: (1) cohomological dimension for groups, (2) Eilenberg-MacLane spaces $K(G,n)$, (3) aspherical CW complexes, and (4) the relationship between these concepts via group cohomology and topological properties. While basic group theory and topology exist in Mathlib, the specialized algebraic topology needed for this conjecture requires substantial new theory development.

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

* ams-55
* ams-20
* ams-18

### 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

Created by AI, reviewed by me.

Start by reading the conjecture description and linked sources, then inspect the repository for existing algebraic topology, group cohomology, and related formalizations. The issue identifies major missing components, including cohomological dimension, Eilenberg–MacLane spaces, and aspherical CW complexes; done requires adding the conjecture in the repository's formal language once the required theory is available.

Written by the indexing model from the issue text.