Zeeman's Conjecture: Collapsibility of Contractible 2-Polyhedron Products

### What is the conjecture

**Zeeman's Conjecture** is a fundamental unsolved problem in piecewise-linear (PL) topology relating two key concepts in combinatorial topology.

**Key Definitions:**
- A polyhedron is **contractible** if its identity map is null-homotopic (can be continuously deformed to a point).
- A polyhedron is **collapsible** if it admits a sequence of elementary collapses reducing it to a point, where an elementary collapse removes a pair of simplices, one of which is a maximal face of the other.
- Collapsibility is a stronger condition than contractibility.

**Conjecture Statement:**

For every contractible 2-polyhedron $K$, the product $K \times I$ is collapsible, where $I = [0,1]$ is the unit interval.

Equivalently: If $G$ is a 2-dimensional CW complex with trivial homology, then some barycentric subdivision of $G \times I$ is collapsible.

**Significance:** The conjecture connects collapsibility and contractibility for low-dimensional complexes and has implications for understanding 3-manifolds and their spines. It remains open, though partial results exist (e.g., Cohen proved $K \times I^6$ is collapsible for contractible 2-polyhedra $K$).

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

**Sources:**
- https://en.wikipedia.org/wiki/Zeeman_conjecture; https://gradmath.org/2021/07/13/zeemans-conjecture/; Alexander Kupers, "Zeeman's Conjecture," The Graduate Journal of Mathematics, Vol. 6, Issue 1 (2021); E.C. Zeeman, "Seminar on combinatorial topology," IHÉS/University of Warwick (1963-1966)

### Prerequisites needed

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

**Building blocks (from Mathlib):**
- `TopologicalSpace` and contractibility theory
- `SimplicialComplex` and basic simplicial topology
- Homotopy equivalence and fundamental concepts

**Missing pieces:**
- Formal definition of elementary collapse and collapsibility for polyhedra in a PL-theoretic framework
- PL topology infrastructure: polyhedra as objects, subdivision operations, collapse sequences

**Rating justification (3/5):** Mathlib has contractibility and basic topology, but lacks the specialized PL combinatorial concepts (elementary collapse, collapsibility) which are not foundational but represent significant new theory needed to state the conjecture precisely. The main work is formalizing PL-specific definitions rather than foundational changes.

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

* ams-55
* ams-57
* 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)