An AI can propose a thousand discoveries in an hour. Which ones are true?
Slean checks it automatically, with the rigour of a mathematical , on simulated where everything can be checked. It is the judge of Mutome’s research .
Step 0 · 11 cars
How it works, in three steps
A world whose exact rules are known
Take the road above. A car moves if the space ahead is free, otherwise it waits. These rules are written once and for all, with no ambiguity: it is an exact .
An AI proposes a claim
An watches the world and puts forward an idea, for example a : a quantity that would never change.
“The number of cars never changes.”
Slean tests it, then proves or refutes it
Slean looks for a . If it finds one, the claim is refuted. Otherwise it takes a proof for every possible road, and the checks it.
Proved: true for every road
Refuted: here is the case where it fails
These worlds are deliberately simple, so that everything can be checked exactly. Real-world science is the long-term goal, not what Slean does today.
Why “Slean”?
Slean = Science + Lean
Lean is a programming language and proof assistant: a small checks every proof. With Mathlib, its shared library, it is why AI now makes real progress in mathematics: a machine can try thousands of proofs, and only the correct ones are accepted.
Slean brings that automatic verification and that cumulative library to scientific discovery, starting with simulated worlds where everything can be checked. Mutome’s agents use it to know what they have really found.
Our inspirations: Lean, Physlib, Wolfram, Minimo and morePlay: guess the law
One minute. Pick what never changes on the road, and watch Slean test it, then prove it.
Step 0 · 11 cars
On this road, what never changes?
What the Lean kernel actually checked
Here is the road’s law, written for Lean. Click a part to see what it means. The accepted it: it is true for roads of every size.
:
Accepted by the kernel, for every ring size
theorem trafficThe name of the claim: “traffic”.Conserved“… never changes”: the total stays the same at every step, on roads of every size.(eca 184)The world: rule 184, the traffic one.(tableFn 2 [0, 1]) 1What is counted: 0 for an empty cell, 1 for a car. The total is the number of cars.:=“and here is why”: the proof starts.conserved_of_fluxCheckProof by local checks: if every small piece of road is in order, the whole road is, whatever its size.(tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1The certificate: how many cars cross each border between two cells, written in Lean’s convention.(by decide +kernel)The computer does every local check, not us, and the Lean kernel checks the result.
Mutome explores. Slean verifies.
The two projects go together. Mutome is an autonomous research lab: its agents try many things, it is randomness in discovery. Slean decides, without appeal, whether what they found is true: it is determinism in verification.
- Mutome
- Randomness in discovery
- Slean
- Determinism in verification
- An agent proposesA law, a structure or a refutation about an exact world.
- Slean verifiesThe Lean kernel accepts the certificate, or a counterexample refutes.
- The library keeps itEach result becomes a reusable theorem.
- The measurement scoresAgainst hidden answers, next to simple methods at equal cost.
Three more games
Each takes a minute or two and shows another side of Slean.
First results
We let an AI loose in labs of 16 unknown worlds, rules hidden, and compared what it finds with a reference program that searches methodically. Same budget, same commands.
Discoveries accepted against experiments spent
Show the data
| Run | Cell updates | Discoveries accepted |
|---|---|---|
| Scripted reference, seed 7 | 199,748 | 88 |
| Claude Sonnet agent, seed 7 | 888 | 90 |
| Scripted reference, seed 11 | 199,802 | 93 |
| Claude Sonnet agent, seed 11 | 1,277 | 98 |
How to read this chart
Each point is one full run in a lab. The higher it is, the more true discoveries it found. The further left, the fewer experiments it needed. The agent (in green) sits at the top left.
Honest reading
The loop and the measurement work: unseen worlds, hidden answers, metered experiments, and no false claim accepted, from anyone.
The agent finds a little more than the reference with 150 to 225 times fewer experiments.
But these worlds can be identified with a single experiment. So we built harder ones, where inferring a short law is the task: there, the agent’s own lessons from earlier labs improved its results on every unseen seed (+7 to +12). One run per seed, so still a first measurement.
All measurements, including the negative onesFour kinds of evidence
“True” can mean four different things. Slean never mixes them: a law proved in a world of cells is not a law of nature.
| Kind | What it means | Example in Slean |
|---|---|---|
| Proved in a world | A Lean theorem about a world’s exact definition. True for that world, unconditionally. | Traffic: the number of cars is conserved for every ring size. |
| Checked computation | A finite fact the kernel evaluated, such as a counterexample or a periodic orbit. | Rule 30’s counterexample 001 → 111; the period-16 glider. |
| Supported by simulation | No counterexample found in a stated search. It is a conjecture, kept as an open brick. | A regularity seen in every simulation tried, without a proof: it stays an open conjecture. |
| Confirmed on the real world | A prediction registered before the data that settles it, evaluated by a frozen rule. It is the only kind that says anything about nature. | None yet. It is milestone M5 on the roadmap. |
A law proved in a cellular automaton is not a law of nature. To move towards physics, Slean makes the gap between the first kind and the last explicit, and never blurs it.