# A finitely generated Eilenberg–Ganea counterexample

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A finitely generated counterexample to the Eilenberg–Ganea conjecture](../../preprints/A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026/paper.pdf)

## Scope

The Eilenberg–Ganea conjecture predicts that a group of integral cohomological dimension two has a two-dimensional classifying space. The formalization constructs a finitely generated residually finite group of cohomological dimension two that has a three-dimensional classifying space but no two-dimensional one. Thus its geometric dimension is three, contradicting the conjecture.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Counterexample to the Eilenberg–Ganea conjecture | [EilenbergGanea.lean](../ComparatorChallenges/EilenbergGanea.lean) |