Library
Everything accepted or refuted is kept as Lean theorems that later research reuses.
Slean’s memory
Every accepted or refuted result becomes a brick in the library. A brick is a Lean theorem: it can be checked again at any time, and reused without redoing it.
There are three kinds of bricks:
- accepted: a law with its checked certificate;
- refuted: a false claim with its checked counterexample;
- open: a conjecture supported by simulation, without a proof. It stays marked as open, never as true.
The first library
The current library holds every conservation law of width at most 3 of the 256 elementary automata, up to trivial ones: 84 laws over 66 rules. Each one is proved for rings of every size. The command lake build re-checks all of them in about twenty seconds.
You can browse them below. Your browser recomputes the automaton from its rule number and adds up the chosen law’s density on every row.
A library law, recomputed in your browser
Rule 184 is a traffic model: a car, a black cell, moves one cell forward when the cell ahead is free. Each row is one time step, top to bottom, on a ring of 64 cells. The library holds one law for this rule: the number of free cells never changes, so neither does the number of cars.
Total of the density: 36 at each of the 40 steps.
- 0
- 1
- 1
- 0
Weight of each pattern read from a cell, as stored in library brick b00047. The numbers to the right of the figure are the total of these weights on the row.
This figure is a simulation: it shows the law on one configuration for 40 steps. The proof holds for every size and every configuration. It is the theorem conserved_of_fluxCheck applied to the flux certificate the kernel checked.
The figure is a simulation on one configuration and 40 steps. The proof holds for every size and every configuration: it is the theorem conserved_of_fluxCheck applied to the certificate the kernel checked.
Reuse
The library is there so that work is not done twice. An explorer can start from the laws already known for a related world. The measurement checks whether that actually helps: it is the comparison between a cold run and a run with the library, described in Measuring a discovery. On conservation laws, memory saved almost nothing, because the cold method is already close to optimal.