The Poincaré sphere $\Sigma(2,3,5)$ is an integral homology 3-sphere

Open

HomologySpheresBoundBalls.hsbb_poincare_is_int_homology_sphere

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

3-manifoldstopology

Let $P = \Sigma(2,3,5) = \{ z \in \mathbb C^3 : z_0^2 + z_1^3 + z_2^5 = 0,\ \|z\| = 1\}$ be the Poincaré dodecahedral space. Then $P$ is a closed topological 3-manifold and

H_n(P;\mathbb Z) \cong H_n(S^3;\mathbb Z) \quad \text{for all } n \ge 0.

This is the implicit premise of the source's example: $P$ is the standard example of an integral homology 3-sphere other than $S^3$ .

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- The Poincaré dodecahedral space `Σ(2,3,5)` is an integral homology 3-sphere. -/
theorem hsbb_poincare_is_int_homology_sphere :
    IsIntHomology3Sphere 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

The Poincaré sphere Σ(2,3,5)\Sigma(2,3,5)Σ(2,3,5) is an integral homology 3-sphere

The Poincaré sphere $\Sigma(2,3,5)$ is an integral homology 3-sphere