A homotopy 3-sphere is homeomorphic to the 3-sphere (Perelman)

Let $M$ be a Hausdorff topological $3$-manifold (a charted space over $\mathbb{R}^3 =$ EuclideanSpace ℝ (Fin 3)). If $M$ is homotopy equivalent to the standard $3$-sphere, then $M$ is homeomorphic to it:

This is the deep half of the three-dimensional topological Poincaré conjecture, proved by Grigori Perelman (2002–2003) using Richard Hamilton's Ricci flow with surgery. It is precisely the $n = 3$ instance of Mathlib's proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere, which asserts for each $n$ that a topological manifold homotopy equivalent to $\mathbb{S}^n$ is homeomorphic to it. Together with the classical fact that a closed simply connected $3$-manifold is a homotopy $3$-sphere, this statement gives the Poincaré conjecture in dimension three.

Formalization Note Here $\simeq_h$ is ContinuousMap.HomotopyEquiv (notation ≃ₕ) and $\simeq_t$ is Homeomorph (notation ≃ₜ); the sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin (3 + 1))) 1. The hypothesis is a bare homotopy equivalence, matching the shape of the sibling proof_wanted; no compactness or simple-connectivity hypothesis is required beyond the homotopy equivalence itself.