Finding the laws of simple worlds, and proving them
We study cellular automata on finite lattices: square, hexagonal and triangular. Each claim goes through a loop of machine checks: a simulation, a test registered in advance, and a proof in Lean. More and more of the proposing and proving is done by AI agents, and machines judge their work too.
A loop in which nobody marks their own work
Finding a pattern in data is easy. Knowing whether it is real is hard: with enough rules, sizes and laws to try, chance supplies patterns too. So every stage of our loop hands its output to a check that the stage cannot change:
- Experiment. LatticeLife runs the automata and says what each number means, including when it is only a bound.
- Law. Kepler fits closed-form laws with error bars, and ranks them against their rivals.
- Registered test. A law's predictions at untested sizes are written to a hash-chained ledger and pushed to GitHub before anyone computes those sizes.
- Proof. What survives is proved in Lean 4. A theorem counts only if it builds and rests on Lean's three standard axioms.
- Agents. AI agents, given a problem card and the proof library, propose the mechanism and write the proof. An automatic judge decides whether it counts.
The model, in detail, includes the real ledger of one study, to check yourself, and a record of every step an agent took.
Registered tests, misses included
predictions written before the runsThree of these tests refuted what we registered. We count that as the method working: each miss pointed at something real, and the corrected claim was then registered and tested again.
| Claim | Tested at | Outcome |
|---|---|---|
| Square parity law, P(n) = 2v(2sord(m) − 1) | 45 sizes by simulation, then all 198 sizes from 3 to 200 exactly | held at all its rival refuted at all 10 sizes where they differ |
| Hexagon parity law, first form | 70 sizes | refuted at 74, 148 and 190, by a factor of 3 |
| Hexagon parity law, corrected | 100 new sizes, 202 to 400 | held at all then proved for every even n |
| Triangle parity laws | 154 sizes | held at all |
| Kepler finds the hexagon law itself | 8 registered expectations | 8 of 8 |
| B2/S34 settling time grows like log L | hexagon tori up to L = 1024, 100 soups each | held the power law rejected (p = 10−9) |
| Kepler's laws for 42 linear rules, 38 never studied | 1,930 new (rule, size) pairs | held every rule with a law kept one |
| Rules that do not split reach the full bound | 113 predictions on 116 new rules | refuted 7 failed, which revealed cubes and dilations |
| The refined statement, as a fixed procedure | 11,358 predictions, 344 new rules | refuted 43 failed (0.4%), which revealed the twisted power |
| The laws the agents proved, at sizes nobody had computed | 15, 40 and 20 predictions in three pilots | 75 of 75 |
| The fourth agent's mechanism for m = 37, at a held-out grid registered before it started | 180 claims at 29 held-out sizes | 180 of 180 |
| The fifth agent's mechanism for m = 25, at a held-out grid registered before it started | 414 claims at 43 held-out sizes, on the atlas and the square family | 414 of 414 |
| Our expectation that the cube confinements left in the square family are chance | all 32,767 rules at 14 sizes, registered before the run | refuted at 6: twisted pairs at four, and 16 rules at m = 37 nobody could then explain |
| The same expectation, with both pilots' mechanisms counted | all 32,767 rules at 17 new sizes, 77 to 125 | refuted at 95, 101 and 111, by exactly the nine rules the sixth agent explained, where it predicted them; nothing else |
What the loop has found
The parity laws
Exact period laws for the parity rule on all three lattices. The hexagon's first law was refuted, and the corrected one is proved for every even n. The square rule escapes the shortfalls of rule 90 and the hexagon shares them exactly; a brief literature search found neither fact.
three rounds, refined twiceThe linear atlas
Periods of 502 linear rules built from neighbour shells. A rule reaches its field's full bound unless something confines its eigenvalues. Four mechanisms do, and three of them were found because a registered prediction failed.
replicatedSettling time
A random soup under B2/S34 settles in a time that grows like the logarithm of the torus size, replicated to L = 1024. Across eight random rules on four lattices the fluctuations share one shape and one ratio, the Gumbel values of extreme-value theory.
6 of 6 acceptedAgents that prove
Six fresh agents, each given only a problem card and the Lean library, proved theorems the library lacked, each passing the judge in its first round. The third found its law from data first. The fourth answered a question nobody had answered; the fifth answered part of a harder one; the sixth answered the question the fifth's test raised.
answered by an agentThe cubes at m = 37
Six rules that none of the known mechanisms touches had every eigenvalue a cube at m = 37, far beyond chance. In the fourth pilot an agent found why, on a question nobody had answered, and proved it in Lean. Its condition made 633 claims at 94 sizes, 180 of them at held-out sizes registered before it started, and none was false.
Lean 4, standard axiomsThe proof library
The bridge from periods to eigenvalues, the bound, the reduction from even sizes to odd, every confinement mechanism, and the agents' three proofs, all checked by Lean against mathlib.