slice_ribbon_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Proved status carries no information about that problem. Do not import it or use it as a dependency.

Slice–ribbon conjecture (Fox, 1962): every smoothly slice knot in $S^3$ is a ribbon knot.

Why this node was retired

The posted statement is

∀ (n : ℕ) (crossing_data : Fin n × Fin n → Bool),
  (∃ (surface_in_B4 : True), True) → (∃ (ribbon_disk : True), True)

Both the hypothesis and the conclusion are ∃ _ : True, True, each closed by ⟨trivial, trivial⟩, so the implication is proved by fun _ _ _ => ⟨trivial, trivial⟩ and asserts nothing. crossing_data is an arbitrary boolean matrix that is never used and never constrained to describe a knot diagram.

No knot, no slice disk in $B^4$, and no ribbon disk occurs in the statement — the two placeholders surface_in_B4 and ribbon_disk are names attached to the proposition True.

What a faithful statement would require

A formalization of knots in $S^3$, of smooth sliceness (a smoothly embedded disk in $B^4$ bounded by the knot), and of ribbon-ness (a slice disk with no local maxima for the radial function), and the implication between the latter two.

No corrected replacement node exists yet.