Frequently asked questions

Is this real science?

Not yet, and we do not claim it is. Slean proves laws in exact worlds and measures whether an agent finds them. A law proved in a cellular automaton is not a law of nature. The aim is to build, on worlds where the truth is known, the tools that will later make it possible to judge discoveries on richer systems. See Four kinds of evidence.

Why cellular automata?

Because they are exact, quick to simulate, and can be generated in any number. For every generated world the complete answer can be computed in advance, which makes an honest score possible. Their laws, conserved quantities and moving structures, have analogues in physics. They are calibration worlds: physics worlds come at milestone M4.

Why Lean if Python already checks?

For a finite fact, such as a counterexample or a glider that comes back after 16 steps, Python’s computation is already exact. The Lean kernel adds an independent guarantee: a second checker, small and heavily tested, that does not share the engine’s bugs. Lean becomes indispensable for universal statements such as “for every ring size”: no simulation can cover them, only a proof can.

How does this relate to Mutome?

Mutome is an autonomous research lab. Mutome brings randomness to discovery, Slean brings determinism to verification. Mutome decides what to explore; Slean says what is true, keeps it, and measures whether the exploring helped. At milestone M3, Slean labs become an autoresearch campaign type, so that Mutome measures its “Harness Lift”, what its harness adds, on worlds with hidden answers, and the library becomes Mutome’s verified memory.

What does not work yet?

• Today’s worlds can be identified with one experiment. This is not yet open-ended discovery. See A hidden world rebuilt.
• One kind of world and two kinds of discovery.
• Two seeds, one run each, one agent model.
• Memory has not shown a gain yet: on conservation laws there was almost nothing to save.
• Claim types are fixed in advance; the agent does not yet choose its own questions.
• Nothing is confirmed on the real world yet.

Is the code open?

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