The Conway knot is not smoothly slice
conway_knot_not_smoothly_slice
Submitter: Kim Morrison.
Notes: Lisa Piccirillo, *The Conway knot is not slice*, Annals of Mathematics 191 (2020). Resolves the last remaining case in the classification of slice knots through 12 crossings. The Conway knot has trivial Alexander polynomial so is topologically slice (Freedman), while Piccirillo's theorem rules out smooth sliceness — pairs with `conway_knot_topologically_slice` for an explicit, low-crossing-number witness to the smooth/topological gap (earlier witnesses such as Akbulut-Matveyev's Whitehead doubles existed). Two holes: `conwayKnot_isSimple` asks the solver to certify that the fixed 78-vertex braid-closure polyline is an embedded simple closed curve (a finite check, e.g. over an exact integer model), and `conway_knot_not_smoothly_slice` is Piccirillo's theorem proper; `conwayKnot` itself is trusted, `sorry`-free data. We'd like to thank Lorenzo Luccioli (using Aristotle) for identifying a mis-formalization of the notion of smoothly slice in an earlier version of this problem.
Source: https://arxiv.org/abs/1808.02923
Informal solution: Piccirillo's strategy: construct a knot K' having the same 0-trace as the Conway knot. The trace-embedding argument then transfers sliceness — if the Conway knot were smoothly slice, K' would be too. Compute Rasmussen's s-invariant of K' (a smooth slice obstruction, via Khovanov homology / Lee's perturbation); show s(K') != 0; conclude both K' and the Conway knot are not smoothly slice. Note that the standard smooth slice obstructions s and tau both vanish on the Conway knot itself, which is why the detour through K' is needed.
/-- **The Conway-knot polyline is a simple closed curve.**
A finite — if laborious — check on the fixed 78-vertex braid-closure
polyline: all vertices distinct, non-adjacent edges disjoint, adjacent
edges meeting only at their shared vertex. This certifies that `conwayKnot`
is a genuine embedded knot — the subject the slice question is about — and
is posed as its own hole so that the proof lives in the submission rather
than as an unchecked field of `conwayKnot`. -/
theorem declaration uses `sorry`conwayKnot_isSimple : conwayKnot.IsSimple := ⊢ conwayKnot.IsSimple
All goals completed! 🐙/-- **Piccirillo, "The Conway knot is not slice."**
The Conway knot 11n34 does not bound a smoothly properly embedded 2-disk
in `ℝ³ × [0, ∞)`. -/
theorem declaration uses `sorry`conway_knot_not_smoothly_slice : ¬ conwayKnot.SmoothlySlice := ⊢ ¬conwayKnot.SmoothlySlice
All goals completed! 🐙Solved by
Not yet solved.