∑math20

A finitely generated Eilenberg–Ganea counterexample

1 paperLean

Constructs a finitely generated residually finite group with integral cohomological dimension two and geometric dimension three, disproving the Eilenberg–Ganea conjecture. It has no two-dimensional classifying space, even with infinitely many cells.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A finitely generated counterexample to the Eilenberg–Ganea conjecture

OpenAI · September 23, 2026

We construct a finitely generated residually finite group of integral cohomological dimension two and geometric dimension three, disproving the Eilenberg–Ganea conjecture.

Read PDF Download Source

Cite

@misc{OAI:A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A finitely generated counterexample to the Eilenberg--Ganea conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026/paper.pdf}{OAI:A-finitely-generated-counterexample-to-the-Eilenberg-Ganea-conjecture-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

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

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

Scope note on GitHub →