Mutome (external site)
Menu

Slean in 5 minutes

Slean’s story in plain language: a world, a claim, a test, a proof. With a game for each step.

The problem

An AI can propose a thousand discoveries in an hour. Some are true, many are not, and all of them sound convincing. To use them, you need a judge that says which ones are true, without being swayed by a good explanation. Slean is that judge.

A world known by heart

To be able to check everything, Slean works in simulated whose exact is known. The first one is a ring road. Each cell is empty or holds a car. At each step, all cars look ahead at the same time: if the cell ahead is free, the car moves, otherwise it waits. Press Play:

Rule 184: traffic

View

Step 16: 14 cars

stepcars0141142143144145146147148149141014111412141314141415141614

carfree cellconserved count

Simulated in your browser, centred convention. The number of cars, on the right, does not change. The proof covers every ring.

These worlds are deliberately simple. Real-world science is the long-term goal, not what Slean does today.

A claim

An AI watches this world and proposes an idea, for example a : “the number of cars never changes”. It is a precise claim: it is either true or false, nothing in between.

Try it yourself: Guess the law, then propose one.

Test, then prove

Slean first looks for a : a road where the claim fails. If it finds one, the claim is refuted for good, and the witness is kept. For the number of cars, it finds none.

But testing is not enough: there are infinitely many roads. It takes a . Here it fits in one idea: a car never vanishes, it moves from one cell to the next. It is enough to check this on the 16 ways to arrange 4 neighbouring cells: that is the . The checks these and derives the law for every road, of every size:

Lean 4
theorem traffic :
    Conserved (eca 184) (tableFn 2 [0, 1]) 1 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1
    (by decide +kernel)

The page Claims and certificates explains why a finite check covers infinitely many sizes.

The loop

Slean’s loop

  1. An agent proposesA law, a structure or a refutation about an exact world.
  2. Slean verifiesThe Lean kernel accepts the certificate, or a counterexample refutes.
  3. The library keeps itEach result becomes a reusable theorem.
  4. The measurement scoresAgainst hidden answers, next to simple methods at equal cost.
Mutome explores, Slean verifies. Nothing enters the library without going through the kernel.
  1. An agent proposes a law, a structure or a refutation.
  2. Slean verifies: a counterexample refutes, a certificate accepted by the kernel proves.
  3. The library keeps the result, for later research to reuse.
  4. The measurement compares the agent with simple methods, at equal cost, on worlds nobody has seen and whose answer is hidden.

Mutome, the autonomous research lab, decides what to explore: it is randomness in discovery. Slean says what is true: it is determinism in verification.

What agents found

In worlds with hidden rules, an agent found every law and more structures than a reference program, with 150 to 225 times fewer experiments, and no false claim. Among its findings, a period-16 glider the reference could not see: Find a glider. Its trick: reading a world’s whole rule with one experiment, as The hidden world shows.

What does not work yet

  • Today’s worlds are too easy: one well-chosen experiment reveals their whole rule. So this is not open-ended discovery yet. The page A hidden world rebuilt shows why.
  • One kind of world, one-dimensional cellular automata.
  • Two suite seeds, one run each, one agent model. See Measuring discovery.
  • Nothing here says anything about the real world. A law proved in a world of cells is not a law of nature. See Four kinds of evidence.

Where to go next