FormalConjectures/Arxiv/0912.2382/CurlingNumberConjecture.lean

GitHub source file

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

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

3 declarations, 1 contain sorry, 0 declared as axioms

The Curling Number Conjecture

Reference: arxiv/0912.2382 The Curling Number Conjecture by Benjamin Chaffin and N. J. A. Sloane

Imports (1)
Imported by 1 file
  1. def Arxiv.«0912.2382».k The curling number Let $S$ be a finite nonempty sequence of integers line 40 source

    Source documentation

    The curling number

    Let $S$ be a finite nonempty sequence of integers. By grouping adjacent terms, it is always possible to write it as $S = X Y Y . . . Y = X Y^k$, where $X$ and $Y$ are sequences of integers and $Y$ is nonempty ($X$ is allowed to be the empty sequence $∅$). There may be several ways to do this: choose the one that maximizes the value of $k$: this $k$ is the curling number of $S$, denoted by $k S$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: List, Int, Nat

    Proof uses: SupSet.sSup, Set.ofPred, Exists, And, Ne, List.nil, Eq, HAppend.hAppend, List.flatten, List.replicate

    3 instances, coercions and auxiliary constants left out.

    noncomputable def k (S : List ℤ) : ℕ :=
…

    Mentions: Arxiv.«0912.2382».S

  2. def Arxiv.«0912.2382».S One starts with any initial sequence of integers $S₀$, and extends it by repeatedly appending the curling number of the current sequence line 49 source

    Source documentation

    One starts with any initial sequence of integers $S₀$, and extends it by repeatedly appending the curling number of the current sequence.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: List, Int, Nat

    2 instances, coercions and auxiliary constants left out.

    noncomputable def S (S₀ : List ℤ) (n : ℕ) : List ℤ :=
…
  3. theorem Arxiv.«0912.2382».curling_number_conjecture The sequence will eventually reach $1$ sorry line 58 source

    Source documentation

    The sequence will eventually reach $1$.

    depends on sorry what this means

    Statement uses: List, Int, Ne, List.nil, Exists, Nat, Eq, Arxiv.«0912.2382».k, Arxiv.«0912.2382».S, OfNat.ofNat

    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 curling_number_conjecture (S₀ : List ℤ) (h : S₀ ≠ []) : ∃ m, k (S S₀ m) = 1 := by
…

    Mentions: Arxiv.«0912.2382».k, Arxiv.«0912.2382».S