Existence of a non-isotopic pair of oriented knots
exists_nonisotopic_knots
Submitter: Kim Morrison.
Notes: Asks for two oriented smooth knots in R^3 that are not ambient-isotopic. The benchmark uses an orientation-sensitive notion of isotopy induced by the parametrizations. Mathlib has no knot-invariant infrastructure, so the model must construct an isotopy invariant from scratch. Suggested: the Alexander polynomial / knot determinant, or the Fox 3-coloring count, both of which distinguish the unknot from the trefoil.
Source: Classical; see https://en.wikipedia.org/wiki/Knot_invariant.
Informal solution: Take K1 = unknot (round circle in the xy-plane) and K2 = right-handed trefoil parametrized as t -> (sin t + 2 sin 2t, cos t - 2 cos 2t, -sin 3t). Construct an ambient-isotopy invariant; the simplest computable choice is the number of Fox 3-colorings of any diagram of K, which counts homomorphisms from the knot group to D_3. The unknot admits 3 such colorings (all monochromatic); the trefoil admits 9. Hence the two knots are not ambient-isotopic.
theorem declaration uses `sorry`exists_nonisotopic_knots : ∃ K₁ K₂ : LeanEval.KnotTheory.Knot, ¬ K₁.Isotopic K₂ := ⊢ ∃ K₁ K₂, ¬K₁.Isotopic K₂
All goals completed! 🐙Solved by
Not yet solved.