Roadmap
Every milestone ends with a measurement. When an explorer fails to beat the generic baselines, the design changes. We do not add interface, scope or vocabulary to compensate.
M1 · Foundation Done
- Cellular automata as Lean worlds, and the flux theorem: a local certificate proves conservation for every size.
- A kernel-checked library: the 84 conservation laws of width at most 3 of the elementary automata.
- An engine with verifier, library, explorers, and a protocol that compares cold runs with runs that use memory.
- Finding: additive conservation laws in one dimension are solved by exact data fitting, 20 laws out of 20 in 24 proposals. This class calibrates the machinery; it does not demonstrate discovery.
M2 · Discovery without a recipe In progress
- Done: metered labs. Any agent works through ./lab; cell updates, proposals, tokens and cost are counted, hidden answers stay outside, transcripts are audited, and results are exported to Lean.
- Done: localised structures as a second kind of discovery, with kernel-checked witnesses and refutations.
- Done: a scripted reference scientist that uses exactly the agent’s interface and budget.
- Done: compressible worlds (1,024-entry rules hiding a short law) where inferring the law is the task. Lessons win 8 of 9 repeated pairs (+6 per lab) and help find compact laws, but only draw level with an inductive scripted reference.
- Worlds that one experiment cannot identify: partial observation, noise, large state spaces.
- Reversibility: an inverse-rule certificate when the rule is reversible, a collision when it is not.
- Isomorphisms as bricks: “world B is world A relabelled”, with a transport theorem, so that one discovered relation proves every law of A again for B. This is the first real dependency between bricks.
- Open claim types: the agent defines its own decidable properties in Lean, and their interest is judged by later use.
- Explorers measured over several seeds against exact data fitting and brute force at equal metered cost.
M3 · Mutome runs on Slean Next
- Slean labs become an autoresearch campaign type in Mutome: Mutome measures its “Harness Lift” on worlds whose answers are hidden.
- The library becomes Mutome’s verified memory: what one campaign established, the next reuses without re-checking it by hand.
- Mutome’s continuous runner calls the engine and writes to a growing library.
- mutome.com shows the live library: bricks, refutations, open conjectures and the dependency graph.
M4 · Physics worlds Next
- Lattice and Hamiltonian systems defined in Lean, reusing Physlib definitions where they exist.
- Exactly conserved quantities of discrete integrators, symmetries, stability statements.
- The loop: simulate, conjecture, prove, or refute with a checked counterexample.
M5 · The real world Next
- Engineering, biology and physics data, with prospective verification: Mutome registers a prediction and its evaluation rule before the deciding data exists, and Slean evaluates it with a frozen evaluator.
- Retrospective benchmarks are allowed only with frozen splits and no repeated scoring on the same held-out data.
What Slean is not trying to be
- A new formal language. Lean is the language.
- A metadata or provenance standard. Provenance is recorded, but it is not the product.
- A hosted service or a public interface ahead of evidence that the engine discovers.
- A copy of Physlib, Mathlib or existing simulation codes. Slean reuses them.