Borel conjecture: Homotopy equivalence implies homeomorphism for closed manifolds

### What is the conjecture

The Borel conjecture states that if two closed manifolds are homotopy equivalent, then they are homeomorphic. More precisely, for a closed $n$-dimensional manifold $M$, any homotopy equivalence $f: M \to N$ with another closed $n$-dimensional manifold $N$ should be a homeomorphism.

A key special case, often stated separately, is the **aspherical case**: if $M$ is a closed aspherical manifold (i.e., all higher homotopy groups vanish), then $M$ is determined up to homeomorphism by its fundamental group. This follows from the fact that the fundamental group and the homotopy type determine the manifold structure.

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

**Sources:**
- https://en.wikipedia.org/wiki/Borel_conjecture

### Prerequisites needed

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

Building blocks (1-3; from search results):
- `Homeomorph` and `Equiv` (homotopy equivalence) exist in Mathlib for general types
- Basic topological structures (closed manifolds) via `Manifold` in Mathlib
- Homotopy type and homotopy equivalence concepts available through algebraic topology libraries

Missing pieces (exactly 2; unclear/absent from search results):
- Formal definition of "closed $n$-dimensional manifold" as a concrete Lean/Mathlib structure (requires manifold theory with dimension constraints and compactness)
- Complete formalization of the higher homotopy group (aspherical manifold) definition and its relationship to the manifold classification problem

Rating justification (1-2 sentences): While `Manifold`, `Homeomorph`, and homotopy equivalence concepts exist in Mathlib, a formal statement of the Borel conjecture requires substantial infrastructure around topological/smooth manifold properties, compactness, and dimension. The conjecture is also highly non-trivial from a formalization perspective, as it bridges topology and geometry in ways that require careful definition of what "closed manifold" means in Lean.

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

* ams-57
* ams-55
* ams-54

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