Existence of a non-isotopic pair of oriented two-component links
exists_nonisotopic_link
Submitter: Kim Morrison.
Notes: Warmup for the knot-theory benchmark. Asks for two oriented smooth two-component links in R^3 that are not ambient-isotopic. The benchmark uses an orientation-sensitive notion of isotopy induced by the parametrizations, so the Gauss linking integral is a natural real-valued invariant distinguishing the unlink (lk = 0) from the Hopf link (lk = +/- 1, depending on orientation choice).
Source: Classical; see https://en.wikipedia.org/wiki/Linking_number.
Informal solution: Take L1 = unlink (two unit circles in parallel planes) and L2 = Hopf link, with explicit orientations induced by the parametrizations. Define lk(K, L) by the Gauss double integral (1/4 pi) int int <K(s) - L(t), K'(s) x L'(t)> / |K(s) - L(t)|^3 ds dt. Prove lk is invariant under ambient isotopy of oriented links by exhibiting it as the integral of a closed 2-form on R^3 minus the origin pulled back along (K, L), so Stokes-style arguments show invariance. Compute lk(unlink) = 0 and choose the Hopf-link orientations so that lk(Hopf) = 1. Conclude L1 and L2 are not ambient-isotopic.
theorem declaration uses `sorry`exists_nonisotopic_link : ∃ L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := ⊢ ∃ L₁ L₂, ¬L₁.Isotopic L₂
All goals completed! 🐙Solved by
• @LorenzoLuccioli with Aristotle (Harmonic) on May 9, 2026 (proof)
• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on May 14, 2026
• @daouid with Antigravity (Multi-Model Ensemble: Gemini 3.1 Pro, Gemini 3 Flash, Claude 4.6 Sonnet/Opus) on May 19, 2026 (proof)
• @GanjinZero with Seed Prover (ByteDance) on May 20, 2026