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:
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.
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link
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:
Prerequisites needed
Formalizability Rating: 4/5 (0 is best) (as of 2026-02-06)
Building blocks (1-3; from search results):
HomeomorphandEquiv(homotopy equivalence) exist in Mathlib for general typesManifoldin MathlibMissing pieces (exactly 2; unclear/absent from search results):
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
Choose either option
This issue was generated by an AI agent and reviewed by me.
See more information here: link
Feedback on mistakes/hallucinations: link