Bounding an integral homology ball is decidable

Open

HomologySpheresBoundBalls.hsbb_goal_int_decidable

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

4-manifoldsdecidabilityopen-problemtopology

Present a closed 3-manifold by a finite simplicial complex $K$ : a list of simplices, each a list of vertex labels in $\mathbb N$ , with geometric realization $|K|$ . There is a computable function $f$ from such lists to $\{\mathtt{true}, \mathtt{false}\}$ such that for every $K$ whose realization is an integral homology 3-sphere,

f(K) = \mathtt{true} \iff |K| \text{ bounds a smooth integral homology 4-ball}.

This formalizes the question is there a complete and computable set of invariants that can determine which homology 3-spheres bound homology 4-balls? A complete computable invariant yields such a decision procedure, and conversely $f$ is itself a complete computable invariant. The problem is open; a proof of the negation would also settle it.

Formalization Note. "Computable" is Mathlib's Computable (partial recursive, total). The behaviour of $f$ on complexes that are not integral homology 3-spheres is unconstrained.

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- **Goal.** There is an algorithm which, given a finite simplicial complex `K` whose
realization is an integral homology 3-sphere, decides whether `|K|` bounds a smooth
integral homology 4-ball. -/
theorem hsbb_goal_int_decidable :
    ∃ f : List (List ℕ) → Bool, Computable f ∧
      ∀ K : List (List ℕ), IsIntHomology3Sphere (realization K) →
        (f K = true ↔ BoundsIntHomologyBall (realization K)) := 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