Prove2Me

Akbulut–Kirby: Σ(2,5,7)\Sigma(2,5,7), Σ(3,4,5)\Sigma(3,4,5), Σ(2,3,13)\Sigma(2,3,13) bound contractible 4-manifolds

Open
HomologySpheresBoundBalls.hsbb_akbulut_kirby

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

4-manifoldsbrieskorn-spherestopology

Each of the Brieskorn homology spheres

Σ(2,5,7),Σ(3,4,5),Σ(2,3,13)\Sigma(2,5,7), \qquad \Sigma(3,4,5), \qquad \Sigma(2,3,13)

bounds a compact smooth contractible 4-manifold (a Mazur manifold). In particular each bounds a smooth integral homology 4-ball.

These were among the first Brieskorn spheres other than S3S^3 shown to bound contractible 4-manifolds.

Preamble
import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold
Formal statement
namespace HomologySpheresBoundBalls

/-- (Akbulut–Kirby) `Σ(2,5,7)`, `Σ(3,4,5)` and `Σ(2,3,13)` bound smooth contractible
4-manifolds (Mazur manifolds). -/
theorem hsbb_akbulut_kirby :
    BoundsContractible (BrieskornSphere 2 5 7) ∧
    BoundsContractible (BrieskornSphere 3 4 5) ∧
    BoundsContractible (BrieskornSphere 2 3 13) := 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