Glossary

World

An exact system whose rules are defined in Lean. Today, a one-dimensional cellular automaton on a ring. See World.

Rule

The table that gives a cell’s new state from its neighbourhood. For the 256 elementary automata it is summed up by a number, such as 184 or 30.

Quiescent state

A state q such that a neighbourhood made entirely of q gives q again. It is a calm background: nothing appears out of nowhere. Localised structures sit on such a background.

Density

A way of counting: a weight for each cell, or for each window of a few cells, added up over the whole ring. A conservation law says this total never changes.

Current (flux)

A number on each border between two cells, saying what crosses it during a step. If the change in every cell equals what comes in minus what goes out, the total is conserved.

Certificate

The finite object that comes with a claim and that the kernel checks. For a conservation law, it is the current. See Claims and certificates.

Refutation

The rejection of a false claim, with a counterexample checked by the kernel. See Refutation.

Witness

The concrete configuration that serves as a finite proof: the counterexample of a refutation, or the block of a structure that comes back.

Brick

A result kept in the library as a Lean theorem: accepted, refuted, or open when it is only supported by simulation.

Library

The set of bricks. It is the memory that later research reuses. See Library.

Lab

The directory an agent works in, with a task description and the ./lab command. See Lab.

Budget

The caps of a run: number of proposals and number of cell updates.

Hidden answer

The complete list of what there is to find in a scored world, computed in advance and kept outside the lab.

Scripted reference

An automatic scientist, with no language model, that uses the same commands and the same budget as the agent. It is the bar to clear.

Cold and warm

A cold run starts from nothing. A warm run starts from the library built on other worlds. The difference measures what memory brings.

Beyond bounds

A verified structure that exceeds the bounds of the hidden answer, for example a period of 16 when the answer stops at 8. See A glider.

Lean kernel

The small program at the heart of Lean that checks every proof. In Slean it decides what is true, never the explorer.