Formal target: Corpus.Arxiv210400502BarkerSequence.barker_conjecture

Every Barker sequence has length at most $13$.

Exact formal statement

∀ (a : List.{0} Int), Corpus.Arxiv210400502BarkerSequence.IsBarkerSequence a → LE.le.{0} (List.length.{0} a) 13

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record