prime_knot_conjecture
Provedgraph-theoryknottheorynumber-theoryopenproblemprovedtopology
Classification of prime knots: Every knot decomposes uniquely into prime knots (proved by Schubert 1949). The enumeration of prime knots by crossing number and characterizing their invariants continues. The exact number of prime knots with n crossings grows exponentially.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem prime_knot_conjecture :
∃ (f : ℕ → List (Fin 3 × Fin 3)) (g : ℕ → ℕ),
(∀ n, g n < g (n + 1)) ∧
∀ n, f n ≠ [] := by
sorrySource