The Rule 30 Prize Problems

The question

centerColumn_not_eventually_periodic. Rule 30 Prize, Problem 1 (non-periodicity). The center column of Rule 30 is not eventually periodic: there is no positive period $p$ and threshold $N$ past which the column repeats with period $p$.

centerColumn_frequency_half. Rule 30 Prize, Problem 2 (equal frequency). Each color occurs on average equally often in the center column: the set of times at which it is black has natural density $1/2$. This is Wolfram's phrasing that the discrete limit of $\mathrm{Total}[c[t]]/t$ as $t\to \infty$ is $1/2$.

Rule 30 is the elementary cellular automaton with local update $c^{\prime }=l\oplus (c\vee r)$, the Boolean rule numbered $30$ by Wolfram. Started from a single black cell on a bi-infinite row, its center column t ↦ (state t) 0 looks random — it was long Mathematica's default pseudorandom generator — yet nothing about that randomness is proven. In 2019 Wolfram offered the Rule 30 Prizes for three questions about it; we formalize the first two.

• Problem 1. Is the center column non-periodic (never eventually periodic)?
• Problem 2. Does each color occur on average equally often, i.e. does the running average of the values converge to $1/2$?

Problem 3 — whether computing the $n$-th cell requires at least $O(n)$ work — is omitted. It is model-relative and has no canonical model-independent phrasing. All three are open.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Other.Rule30 (2 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem centerColumn_not_eventually_periodic :
    answer(sorry) ↔
      ¬ ∃ p : ℕ, 0 < p ∧ ∃ N : ℕ, ∀ t : ℕ, N ≤ t → centerColumn (t + p) = centerColumn t

theorem centerColumn_frequency_half :
    answer(sorry) ↔ {t : ℕ | centerColumn t}.HasDensity (1 / 2)

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• Announcing the Rule 30 Prizes, Stephen Wolfram, 2019.
• Rule 30 Prizes.
• Wikipedia: Rule 30.

Source and licence

Imported from Formal Conjectures (Other), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.