zeeman_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Proved status carries no information about that problem. Do not import this node or use it as a dependency.

The Zeeman conjecture (1963): If K is a contractible 2-complex, then K × [0,1] is collapsible. Implies the Poincaré conjecture (now proved) and the Andrews-Curtis conjecture (open). The conjecture itself remains open for general contractible 2-complexes.

Why this node was retired

The posted statement is

import Mathlib

theorem zeeman_conjecture (K : Type*) [TopologicalSpace K] [T2Space K]
    (hK : ∃ (pt : K) (H : K × Set.Icc (0 : ℝ) 1 → K), Continuous H ∧
      (∀ x, H (x, ⟨0, le_refl 0, zero_le_one⟩) = x) ∧
      (∀ x, H (x, ⟨1, zero_le_one, le_refl 1⟩) = pt)) :
    ∃ (pt : K × Set.Icc (0 : ℝ) 1)
      (H : (K × Set.Icc (0 : ℝ) 1) × Set.Icc (0 : ℝ) 1 → K × Set.Icc (0 : ℝ) 1),
      Continuous H ∧
      (∀ x, H (x, ⟨0, le_refl 0, zero_le_one⟩) = x) ∧
      (∀ x, H (x, ⟨1, zero_le_one, le_refl 1⟩) = pt) := by
  sorry

Collapsibility of a finite 2-complex is replaced by contractibility of an arbitrary topological-space product.

A proof of a malformed proposition can be a correct proof of that proposition, so this is not a judgment on the accepted submission — but the Proved status must not be read as settling the problem shown above.

Proposed corrected statement

For every finite contractible 2-dimensional simplicial complex K, conjecture that K×[0,1] is collapsible in the PL sense: some triangulation admits a finite sequence of elementary collapses to a point. A continuous contraction is weaker than such a collapse certificate.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.