Much of the recent progress of AI in mathematics has happened in one place: proofs written in Lean. I do not think that is an accident. Lean gives a model what most research lacks: an answer to the question “is this right?” that does not depend on anyone’s opinion.
Mutome needs something similar for science. Slean is my attempt to build it, starting with small worlds. This essay explains what Slean is, what we measured with it, and what it does not show yet.
What Lean gives mathematics.
Lean is a programming language in which definitions are exact and proofs are checked by a small trusted program, the kernel. A model can propose a thousand proof attempts. The kernel accepts the correct ones and rejects the rest, without getting tired and without being impressed.
Three things follow. The verifier is automatic, so the search can be wide. Results accumulate: Mathlib, the shared library, lets each new proof build on everything already checked. And the frontier is explicit: at any moment, we know exactly which statements are proved.
This is what I mean by randomness in discovery and determinism in verification. In mathematics, Lean supplies the determinism.
Science has no kernel.
Empirical science does not work this way. A claim about nature rests on measurements, models and the judgment of the people who check them. No program can read a paper and decide whether its conclusion is true. Experiments are noisy, instruments have limits, and two explanations can fit the same data.
Software will not fix that. But it makes a self-improving research system hard to measure. If nothing can say exactly whether a discovery is right, we cannot tell whether the system got better at making discoveries or only better at sounding convincing.
What Slean is.
Slean stands for Science + Lean. Instead of starting with nature, it starts with worlds defined exactly in Lean. Today, these are cellular automata: grids of cells that change by a fixed local rule. They are simple, but they have laws, structures and mechanisms to discover, and every claim about them has a precise meaning.
A claim counts only when it is checked exactly. A law, a structure or a short formula that computes a world’s whole rule is accepted when the Lean kernel checks it. A proposed mechanism is checked by exact comparison with the world. A refutation comes with a counterexample, which is checked too. Accepted results join a library that later work can build on.
Slean also has labs. In a lab, an agent studies a world whose answers are hidden. It can act only through a ./lab command that counts every experiment. At the end, its claims are scored against the hidden answers and compared with a scripted reference that had exactly the same budget.
These labs are how Mutome will measure itself. If a change to Mutome’s harness helps, it should help on labs it has never seen. If it does not, the change should not be kept.
What we measured.
The first lesson was humbling. Conservation laws, the classic thing to find in these worlds, are solved completely by a generic method of about fifty lines that fits the data exactly. That class of problems helps calibrate the engine. It cannot demonstrate an ability to discover.
On generated worlds with hidden rules, a Claude Sonnet agent found every hidden conservation law and slightly more structures than the scripted reference. It used 150 to 225 times fewer experiments and made no false claim. That sounds good, but each of those worlds can be identified with a single well-chosen experiment. It is competent work, not open-ended discovery.
We then gave the agent lessons kept from earlier labs. On that battery, they changed the results by 0 and by +1 discovery. The battery was saturated: there was no room left for an improvement to show.
So we built harder worlds, which we call compressible: rules with 1,024 entries that hide a short law, and a tight experiment budget. On a first run, the agent alone made 3 discoveries out of 48, against 12 for the scripted reference. It never tried to infer the short law.
On three held-out seeds, the same agent with lessons kept from earlier labs made 13, 13 and 17 verified discoveries, against 4, 6 and 5 without them. We ran the whole comparison three times. Lessons won in 8 pairs out of 9, by 6 discoveries per lab on average. It is the first change to Mutome’s harness that improved results on worlds it had never seen.
Then we let the agent submit compact laws: a short formula that computes a world’s whole rule, which the Lean kernel checks on all 1,024 neighbourhoods. Finding one requires inferring the rule rather than reading it. With lessons, the agent found 8, 12 and 8 of the 12 hidden laws. Without them, it found 2, 6 and 5.
Then the result became humbling again. We rewrote the scripted reference so that it tries the textbook families of rules, such as linear and totalistic rules. It found 9 laws and 47 to 54 discoveries per lab. With lessons, the agent is level with it. Without them, it falls behind on two seeds out of three. Part of what lessons teach may simply be which families this suite uses, so the next worlds must use families outside that list.
What it does not show.
None of this is a discovery about the real world. These worlds are toys by design: small enough to be checked exactly, which is the point. A law proved in a cellular automaton says nothing about nature, and an improvement measured here is not yet an improvement in real research.
It does not show that Mutome improves itself either. It shows one improvement, repeated on a battery built to detect it, and a simple script that does as well. That is a beginning I can measure, which is what I wanted.
What comes next.
The next step is to let Mutome run Slean labs continuously, within a budget of $50 a month, and to change its own harness only when the change improves results on labs it has not seen. Then come worlds closer to physics, and later, predictions about the real world made before the data exists, so they can be checked without hindsight.
If you want to see what these worlds feel like, slean.org explains them in plain language, and its four mini-games let you look for the laws of a world yourself. The measurements are published there too, including the ones that do not flatter us.