Install and check

Build the Lean library, run the engine tests and check a first law.

Access

The Slean repository is private for now. Access is given on request.

Requirements

Lean, installed with elan.
Python 3.11 or newer. The engine has no dependencies.

Check the library

At the root of the repository:

Terminal

lake build

This has the Lean kernel check Slean’s core and the 84 laws of the library, in about twenty seconds. Only the standard axioms are used.

Run the engine tests

Terminal

cd engine
python3 -m unittest discover -s tests

These tests check the engine, and the agreement between the engine and the Lean definitions.

Check a first law

Terminal

python3 -m slean check 184 1 0,1

The question asked: in rule 184, is the width-1 density that is 0 for an empty cell and 1 for a car conserved? In other words, does the number of cars change? The engine answers with a verdict in JSON, certified here, with the current it found, then prints the matching Lean theorem. With a false claim, such as python3 -m slean check 30 1 0,1, the verdict is refuted and the theorem contains the counterexample.

The printed current may differ by a constant from the one on the Traffic page: both are valid.