Prove2Me

Fintushel–Stern: Σ(2,3,7)\Sigma(2,3,7) bounds a rational homology ball

Open
HomologySpheresBoundBalls.hsbb_fintushel_stern

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

4-manifoldsbrieskorn-spherestopology

The Brieskorn homology sphere

Σ(2,3,7)={z∈C3:z02+z13+z27=0, ∥z∥=1}\Sigma(2,3,7) = \{ z \in \mathbb C^3 : z_0^2 + z_1^3 + z_2^7 = 0,\ \|z\| = 1 \}

bounds a compact smooth rational homology 4-ball.

Its Rokhlin invariant is nontrivial, so it bounds no integral homology ball; this example separates the rational and integral versions of the question.

Preamble
import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold
Formal statement
namespace HomologySpheresBoundBalls

/-- (Fintushel–Stern) The Brieskorn sphere `Σ(2,3,7)` bounds a smooth rational homology 4-ball. -/
theorem hsbb_fintushel_stern : BoundsRatHomologyBall (BrieskornSphere 2 3 7) := 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