Rokhlin: the Poincaré sphere bounds no smooth integral homology ball

Open

HomologySpheresBoundBalls.hsbb_rokhlin_poincare

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

4-manifoldsrokhlin-invarianttopology

Let $P = \Sigma(2,3,5)$ be the Poincaré homology sphere. There is no compact smooth 4-manifold $W$ with boundary such that $H_n(W;\mathbb Z) \cong H_n(\mathrm{pt};\mathbb Z)$ for all $n$ and $\partial W$ is homeomorphic to $P$ :

P \text{ does not bound a smooth integral homology 4-ball.}

The obstruction is the Rokhlin invariant, which is nontrivial for $P$ . The statement is false in the topological category (Freedman), so smoothness of $W$ is essential.

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- (Rokhlin) The Poincaré homology sphere does not bound a smooth integral homology 4-ball. -/
theorem hsbb_rokhlin_poincare : ¬ BoundsIntHomologyBall PoincareSphere := by sorry

end HomologySpheresBoundBalls

Source

Open Problem Garden, 'Which homology 3-spheres bound homology 4-balls?' (rybu, 2009), http://www.openproblemgarden.org/op/which_homology_3_spheres_bound_homology_4_balls

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph