SnakeInTheBox.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

15 declarations, 6 contain sorry, 0 declared as axioms

Snake in the box

References:

Wikipedia
Hypercube
xkcd
[DK67] L. Danzer and V. Klee, Lengths of snakes in boxes, Journal of Combinatorial Theory 2 (1967), 258–265.
[Ze97] G. Zémor, An upper bound on the size of the snake-in-the-box, Combinatorica 17 (1997), 287–298.

Imports (1)

FormalConjecturesUtil

def SnakeInBox.Hypercube A graph on the power set of Fin n, where two sets are adjacent if they differ by a single element line 44 source
Source documentation
A graph on the power set of Fin n, where two sets are adjacent if they differ by a single element.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, SimpleGraph, Finset, Fin
Proof uses: SimpleGraph.fromRel, Eq, Finset.card, symmDiff, OfNat.ofNat
6 instances, coercions and auxiliary constants left out.
```
def Hypercube (n : ℕ) : SimpleGraph (Finset (Fin n)) := fromRel fun a b => (a ∆ b).card = 1
```
def SnakeInBox.IsSnakeInGraphOfLength A subgraph G' is a 'snake' of length k in graph G if it is an induced path of length k line 49 source
Source documentation
A subgraph G' is a 'snake' of length k in graph G if it is an induced path of length k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Subgraph, Nat
Proof uses: And, SimpleGraph.Subgraph.IsInduced, Exists, SimpleGraph.Walk, SimpleGraph.Walk.IsPath, Eq, SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.length
```
def IsSnakeInGraphOfLength {V : Type u} [DecidableEq V] (G : SimpleGraph V) (G' : Subgraph G)
    (k : ℕ) : Prop :=
…
```
def SnakeInBox.LongestSnakeInGraph The length of the longest induced path (or 'snake') in a graph G line 56 source
Source documentation
The length of the longest induced path (or 'snake') in a graph G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, SimpleGraph.Subgraph, SnakeInBox.IsSnakeInGraphOfLength
1 instances, coercions and auxiliary constants left out.
```
noncomputable def LongestSnakeInGraph {V : Type u} [DecidableEq V] (G : SimpleGraph V) : ℕ :=
…
```
def SnakeInBox.LongestSnakeInTheBox The length of the longest snake for the Hypercube n graph line 62 source
Source documentation
The length of the longest snake for the Hypercube n graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SnakeInBox.LongestSnakeInGraph, Finset, Fin, SnakeInBox.Hypercube
2 instances, coercions and auxiliary constants left out.
```
noncomputable def LongestSnakeInTheBox (n : ℕ) : ℕ := LongestSnakeInGraph <| Hypercube n
```
Mentions: SnakeInBox.LongestSnakeInGraph, SnakeInBox.Hypercube
def SnakeInBox.IsCoilInGraphOfLength A subgraph G' is a 'coil' of length k in graph G if it is an induced cycle of length k line 67 source
Source documentation
A subgraph G' is a 'coil' of length k in graph G if it is an induced cycle of length k.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, SimpleGraph.Subgraph, Nat
Proof uses: And, SimpleGraph.Subgraph.IsInduced, Exists, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, Eq, SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.length
```
def IsCoilInGraphOfLength {V : Type u} [DecidableEq V] (G : SimpleGraph V) (G' : Subgraph G)
    (k : ℕ) : Prop :=
…
```
def SnakeInBox.LongestCoilInGraph The length of the longest induced cycle (or 'coil') in a graph G line 74 source
Source documentation
The length of the longest induced cycle (or 'coil') in a graph G.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: DecidableEq, SimpleGraph, Nat
Proof uses: SupSet.sSup, Set.ofPred, Exists, SimpleGraph.Subgraph, SnakeInBox.IsCoilInGraphOfLength
1 instances, coercions and auxiliary constants left out.
```
noncomputable def LongestCoilInGraph {V : Type u} [DecidableEq V] (G : SimpleGraph V) : ℕ :=
…
```
def SnakeInBox.LongestCoilInTheBox The length of the longest coil for the Hypercube n graph line 80 source
Source documentation
The length of the longest coil for the Hypercube n graph.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: SnakeInBox.LongestCoilInGraph, Finset, Fin, SnakeInBox.Hypercube
2 instances, coercions and auxiliary constants left out.
```
noncomputable def LongestCoilInTheBox (n : ℕ) : ℕ := LongestCoilInGraph <| Hypercube n
…
```
Mentions: SnakeInBox.LongestCoilInGraph, SnakeInBox.Hypercube
theorem SnakeInBox.snake_zero_zero 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 line 87 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SnakeInBox.LongestSnakeInTheBox, OfNat.ofNat
Proof uses: id, SnakeInBox.LongestSnakeInGraph, Finset, Fin, SnakeInBox.Hypercube, SupSet.sSup, Set.ofPred, Exists, SimpleGraph.Subgraph, SnakeInBox.IsSnakeInGraphOfLength, And, SimpleGraph.Subgraph.IsInduced, SimpleGraph.Walk, SimpleGraph.Walk.IsPath, SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.length, Eq.mpr, SimpleGraph.fromRel, Finset.card, symmDiff and 48 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem snake_zero_zero : LongestSnakeInTheBox 0 = 0 := by
…
```
Mentions: SnakeInBox.LongestSnakeInTheBox
theorem SnakeInBox.coil_zero_zero The longest coil in the $0$-dimensional cube is zero, since it contains no cycles line 104 source
Source documentation
The longest coil in the $0$-dimensional cube is zero, since it contains no cycles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, SnakeInBox.LongestCoilInTheBox, OfNat.ofNat
Proof uses: id, SnakeInBox.LongestCoilInGraph, Finset, Fin, SnakeInBox.Hypercube, SupSet.sSup, Set.ofPred, Exists, SimpleGraph.Subgraph, SnakeInBox.IsCoilInGraphOfLength, And, SimpleGraph.Subgraph.IsInduced, SimpleGraph.Walk, SimpleGraph.Walk.IsCycle, SimpleGraph.Walk.toSubgraph, SimpleGraph.Walk.length, Eq.mpr, SimpleGraph.fromRel, Finset.card, symmDiff and 28 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem coil_zero_zero : LongestCoilInTheBox 0 = 0 := by
…
```
Mentions: SnakeInBox.LongestCoilInTheBox
theorem SnakeInBox.snake_small_dimensions 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$ sorry line 125 source
Source documentation
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$.

depends on sorry what this means
Statement uses: Eq, List, Nat, List.map, SnakeInBox.LongestSnakeInTheBox, List.range, OfNat.ofNat, List.cons, List.nil
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem snake_small_dimensions :
    map LongestSnakeInTheBox (range 9) = [0, 1, 2, 4, 7, 13, 26, 50, 98] := by
…
```
Mentions: SnakeInBox.LongestSnakeInTheBox
theorem SnakeInBox.coil_small_dimensions The maximum length for the coil-in-the-box problem is known for dimensions zero through eight; it is $0, 0, 4, 6, 8, 14, 26, 48, 96$ sorry line 134 source
Source documentation
The maximum length for the coil-in-the-box problem is known for dimensions zero through eight; it is $0, 0, 4, 6, 8, 14, 26, 48, 96$.

depends on sorry what this means
Statement uses: Eq, List, Nat, List.map, SnakeInBox.LongestCoilInTheBox, List.range, OfNat.ofNat, List.cons, List.nil
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem coil_small_dimensions :
    map LongestCoilInTheBox (range 9) = [0, 0, 4, 6, 8, 14, 26, 48, 96] := by
…
```
Mentions: SnakeInBox.LongestCoilInTheBox
theorem SnakeInBox.snake_dim_nine For dimension $9$, the length of the longest snake in the box is not known sorry line 143 source
Source documentation
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.

depends on sorry what this means
Statement uses: Eq, Nat, SnakeInBox.LongestSnakeInTheBox, OfNat.ofNat, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem snake_dim_nine : LongestSnakeInTheBox 9 = answer(sorry) := by
…
```
Mentions: SnakeInBox.LongestSnakeInTheBox
theorem SnakeInBox.snake_dim_nine_lower_bound The best length found so far for dimension nine is 190 sorry line 150 source
Source documentation
The best length found so far for dimension nine is 190.

depends on sorry what this means
Statement uses: LE.le, Nat, OfNat.ofNat, SnakeInBox.LongestSnakeInTheBox
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem snake_dim_nine_lower_bound : 190 ≤ LongestSnakeInTheBox 9 := by
…
```
Mentions: SnakeInBox.LongestSnakeInTheBox
theorem SnakeInBox.snake_upper_bound For $n \geq 1$, an upper bound on the length of the longest snake in a box is $2^{n-1}$ (see [DK67, Theorem B]) sorry line 160 source
Source documentation
For $n \geq 1$, an upper bound on the length of the longest snake in a box is $2^{n-1}$ (see [DK67, Theorem B]).

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, SnakeInBox.LongestSnakeInTheBox, HPow.hPow, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem snake_upper_bound (n : ℕ) (hn : 1 ≤ n) : LongestSnakeInTheBox n ≤ 2 ^ (n - 1) := by
…
```
Mentions: SnakeInBox.LongestSnakeInTheBox
theorem SnakeInBox.coil_upper_bound For $n \geq 2$, an upper bound on the maximal length of the longest coil in a box is given by $$ 1 + 2^{n-1}\frac{6n}{6n + \frac{1}{6\sqrt{6}}n^{\frac 1 2} - 7} $$ (see [Ze97]) sorry line 171 source
Source documentation
For $n \geq 2$, an upper bound on the maximal length of the longest coil in a box is given by $$ 1 + 2^{n-1}\frac{6n}{6n + \frac{1}{6\sqrt{6}}n^{\frac 1 2} - 7} $$ (see [Ze97]). The case $n = 1$ is excluded since the right-hand side is negative there.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Real, SnakeInBox.LongestCoilInTheBox, HAdd.hAdd, HDiv.hDiv, HMul.hMul, HPow.hPow, HSub.hSub, Real.sqrt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem coil_upper_bound (n : ℕ) (hn : 2 ≤ n) : LongestCoilInTheBox n
    ≤ (1 : ℝ) + 2 ^ (n - 1) * (6 * n) / (6 * n + (1 / (6 * √6) * √n) - 7) := by
…
```
Mentions: SnakeInBox.LongestCoilInTheBox