Formal target: Corpus.Arxiv09122382CurlingNumberConjecture.curling_number_conjecture

The sequence will eventually reach $1$.

Exact formal statement

∀ (S₀ : List.{0} Int),
  Ne.{1} S₀ List.nil.{0} →
    Exists.{1} fun m =>
      Eq.{1} (Corpus.Arxiv09122382CurlingNumberConjecture.k (Corpus.Arxiv09122382CurlingNumberConjecture.S S₀ m)) 1

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record