snake_dim_nine

The longest snake in the $0$-dimensional cube, i.e. the cube consisting of one point, is zero, since there only is one induced path and it is of length zero. -/ @[category test, AMS 5] theorem snake_zero_zero : LongestSnakeInTheBox 0 = 0 := by simp_rw [LongestSnakeInTheBox, LongestSnakeInGraph, IsSnakeInGraphOfLength, Hypercube] convert csSup_singleton 0 ext n refine ⟨fun ⟨S, ⟨h_induced, ⟨u, ⟨v, ⟨P, ⟨hPath, hSupport, hLength⟩⟩⟩⟩⟩⟩ ↦ ?_, fun h ↦ ?_⟩ · have hu := Finset.eq_empty_of_isEmpty u have hv := Finset.eq_empty_of_isEmpty v subst hu hv simp_all · rw [h] use (⊤ : Subgraph _), by simp, ∅, ∅ simp open List /- The maximum length for the snake-in-the-box problem is known for dimensions zero through eight; it is $0, 1, 2, 4, 7, 13, 26, 50, 98$. --/ @[category research solved, AMS 5] theorem snake_small_dimensions : map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98] := by sorry /- For dimension $9$, the length of the longest snake in the box is not known. This is currently the smallest dimension where this question is open. -

theorem snake_dim_nine : LongestSnakeInTheBox 9 = answer(sorry)

Recent Submissions

No submissions yet. Be the first to attempt this problem.