How to Start on the Rule 30 Prize
How to Start on the Rule 30 Prize
The Rule 30 Prize kit • 2026
Rule 30 is one line of Boolean logic, yet its center column looks random, and nobody can prove anything about that randomness. This essay sets up the tools for the three Rule 30 Prize problems. It computes the pattern and its center column in the Wolfram Language. It loads the official Lean statements with LeanLink and checks that Lean's definition computes the same column. It proves a first, known result in the exact form the verifier reads, and it shows what the checks catch. It ends with how to write and submit an essay of your own.
The question
The question
Rule 30 updates every cell from itself and its two neighbors: the new color is left XOR (center OR right). Started from a single black cell, it grows a pattern that is regular on its left edge and looks random almost everywhere else.
The first 80 steps, with the center column in red:
In[]:=
pattern=CellularAutomaton[30,{{1},0},80];ArrayPlot[ReplacePart[pattern,{t_,81}:>2pattern[[t,81]]],ColorRules->{0->White,1->GrayLevel[0.15],2->StandardRed},ImageSize->520]
Out[]=
The Rule 30 Prizes ask three questions about that red column:
1
.Does the center column always remain non-periodic?
2
.Does each color of cell occur on average equally often in the center column?
3
.Does computing the nth cell of the center column require at least O(n) computational effort?
Each carries a $10,000 prize, under the rules at rule30prize.org. All three have been open since 2019.
The center column
The center column
The column itself is cheap to compute far out.
The first 100,001 cells of the center column, and the first 40 of them:
In[]:=
center=CellularAutomaton[30,{{1},0},{10^5,{{0}}}];Take[center,40]
Out[]=
{1,1,0,1,1,1,0,0,1,1,0,0,0,1,0,1,1,0,0,1,0,0,1,1,1,0,1,0,1,1,1,0,0,1,1,1,0,1,0,1}
Problem 2 asks whether black and white are equally frequent. Count +1 for black and -1 for white, and the running total wanders like a random walk around zero. The walk:
In[]:=
ListLinePlot[Accumulate[2center-1],PlotLabel->"black minus white",ImageSize->520]
Out[]=
Problem 1 asks whether the column is eventually periodic. Here is a quick experiment, which proves nothing.
Periods from 1 to 1000 that fit the second half of the first 100,001 cells:
In[]:=
Select[Range[1000],center[[50001;;-1-#]]===center[[50001+#;;]]&]
Out[]=
{}
None does. A proof has to rule out every period, from every starting time.
The official statements in Lean
The official statements in Lean
The Rule 30 Prize kit, WolframInstitute/Rule30PrizeKit, is a Lean 4 project. It holds the official statements, about 400 proved theorems of partial results, and 96 proved equivalent forms of Problem 1. The verifier checks every submission against exactly this project. LeanLink loads it into the Wolfram Language.
Load LeanLink, point it at the kit (set , or edit the fallback path), and check that the kit is there:
RULE30PRIZE_KIT
In[]:=
Needs["Wolfram`LeanLink`"];$Rule30PrizeKit=Replace[Environment["RULE30PRIZE_KIT"],$Failed->FileNameJoin[{$HomeDirectory,"Rule30PrizeKit"}]];DirectoryQ[$Rule30PrizeKit]
Out[]=
True
The module that states the problems, keeping only its own constants:
In[]:=
statements=LeanImport["Ruliology.CellularAutomata.Rule30Prize","ProjectDir"->$Rule30PrizeKit,"Filter"->"Rule30Prize."]
Out[]=
LeanEnvironment
Problem1
In[]:=
statements["Ruliology.CellularAutomata.Rule30Prize.Problem1"]["TermForm","Open"->{"Ruliology.CellularAutomata.Rule30Prize","Ruliology.CellularAutomata.Rule30Jen"}]
Out[]=
¬EventuallyPeriodic center
Problem2
In[]:=
statements["Ruliology.CellularAutomata.Rule30Prize.Problem2"]["TermForm","Open"->{"Ruliology.CellularAutomata.Rule30Prize"}]
Out[]=
∀ (k : Nat), 0 < k → ∃ N, ∀ (n : Nat), N ≤ n → k * (2 * ↑(blackCount n) - ↑n).natAbs ≤ n
The Lean definition is meant to be checked, not run: it recomputes every cell from scratch, which takes about 3^t steps at time t. For a few cells it is fast enough to compare with .
CellularAutomaton
The first 12 cells, computed by Lean, against the Wolfram Language's:
In[]:=
LeanEvaluate["(List.range 12).map Ruliology.CellularAutomata.Rule30Prize.center","ProjectDir"->$Rule30PrizeKit,"Imports"->{"Ruliology.CellularAutomata.Rule30Prize"}]===(Take[center,12]/.{1->True,0->False})
Out[]=
True
A first result, in the submission format
A first result, in the submission format
A submission's formal proof is the in the symbol . The verifier evaluates the notebook from top to bottom, reads , and rebuilds and checks the Lean source behind it in the kit. Here the same environment lets the essay examine its own proof.
LeanEnvironment
rule30Submission
rule30Submission
The cell with a known result, the case of period 1. The center column is never eventually constant, by Jen's theorem that no two columns of rule 30 are both eventually periodic:
In[]:=
rule30Submission=LeanImportString["import Rule30PrizeKitnamespace Rule30Submissionopen Ruliology.CellularAutomata.Rule30Prize/-- The center column is not eventually constant: Problem 1 for period 1. -/theorem no_period_one : ¬ ∃ N, ∀ t, N ≤ t → center (t + 1) = center t := center_not_eventually_period_oneend Rule30Submission","ProjectDir"->$Rule30PrizeKit]
Out[]=
LeanEnvironment
The theorem's statement, as Lean prints it:
In[]:=
rule30Submission["Rule30Submission.no_period_one"]["TypeForm","Open"->{"Ruliology.CellularAutomata.Rule30Prize"}]
Out[]=
¬∃ N, ∀ (t : ℕ), N ≤ t → center (t + 1) = center t
The axioms it depends on are the three standard ones and nothing else:
In[]:=
rule30Submission["Rule30Submission.no_period_one"]["Axioms"]
Out[]=
{Classical.choice,Quot.sound,propext}
The kernel accepts every declaration of the module again. This is the replay the verifier runs:
In[]:=
rule30Submission["Rule30Submission.no_period_one"]["KernelCheck"]
Out[]=
Success
The lemmas it rests on, two levels down:
What the checks catch
What the checks catch
Suppose a claimed proof of Problem 1 has a gap.
Its type is exactly the official statement, and its axioms give it away:
Building on what is known
Building on what is known
Much is already proved. A submission should build on it, and must not present it as new.
The catalog's lower bound on transient plus period, for any eventual period of the center column:
One of the 96 equivalent forms. Problem 1 holds exactly when the binary number 0.c(0)c(1)c(2)… is irrational:
Your essay, and your submission
Your essay, and your submission
lake build Rule30Submission && lake env lean --run Check.lean Rule30Submission --claim problem1
What this essay does not do
What this essay does not do
It proves nothing new. The period-1 result is Jen's theorem from 1986, and the experiments with periods prove nothing. The essay only sets up the tools, and shows the form in which a new result reaches the verifier and the reviewers.
References
References
[2] E. Jen, Global properties of cellular automata, Journal of Statistical Physics 43 (1986) 219-242.