Machines decide what counts
Our results come out of a loop with five stages. A simulation suggests a law, a fitting engine names it, its predictions are locked in a ledger before the runs that test them, what survives is proved in Lean, and AI agents increasingly propose the mechanisms and write the proofs. At every stage a claim's status comes from a check that whoever made it, person or model, cannot change.
The loop
select a stageWhy it is built this way
Two failures shape the design. The first is the old one of empirical science: with enough rules, sizes and candidate laws, some pattern will fit by chance, and choosing the test after seeing the data makes any law look good. The cure is to register. Before a single test size is computed, the predictions are written down, committed and pushed, and the harness refuses to start the run until they are.
The second failure is new. A language model can write a convincing account of work it did not do, or a proof that only looks right. So an agent's report is never the evidence. The evidence is a build that Lean accepts, a statement that matches a pinned copy, and an axiom list that is Lean's own three, checked by a judge the agent cannot edit.
Between them, these checks let us hand more of the work to agents without trusting them more.
| Role | Who | What it decides |
|---|---|---|
| Direction | the lead researcher | which questions to pursue, and what is published |
| Orchestrator | a Claude Code session working with the lead | designs the studies, writes problem cards, tools and judges, registers predictions, audits the agents |
| Proposer and prover | a fresh Claude Code session per pilot, with only a problem card | proposes a mechanism, checks it numerically, writes the Lean proof |
| Judges | LatticeLife, Kepler, the ledger, Lean and each pilot's judge.py | whether anything counts |
Check a ledger yourself
Every registered study keeps an append-only ledger. Each entry holds the SHA-256 hash of the entry before it, and its own hash covers its content and that link, so changing any entry breaks every link after it. Below is the real ledger of the third pilot's registered test: the question, 20 predictions, the start of the run, the observations and the verdict. Your browser recomputes every hash now.
Edit an entry and the chain breaks there. A forger could recompute every later hash, and the Forge button does just that. This is why the ledger is pushed to GitHub before the run: the remote's history fixes every hash, so a rebuilt chain no longer matches what was published.
Pilot 3's ledger, llm-pilot-vot13
The agents, step by step
In each pilot a fresh agent gets a problem card, the Lean library and a few generic tools, in a cloud container that holds nothing else: an orphan branch with one commit, no write-ups and no hand proofs. It works alone. When it reports, the judge runs; if the judge rejects the work, only the judge's output goes back to the agent.
The chart shows every tool call the agents in pilots 2 to 6 made, read from the session transcripts on the server, not from anything the agents wrote. In pilots 2 and 3 the agents wrote their whole proof within ten minutes, then waited half an hour or more for mathlib to compile in their fresh containers. In pilots 4 and 5, on open questions, the agents had their mechanisms after 23 minutes and spent the rest of their time checking and proving them; the fifth also spent it looking for more, and reported what it could not explain. The sixth found its factorisation in 11 minutes and finished in 66. Pilot 1's agent ran inside the orchestrator's container, so it has no separate transcript.
Tool calls, by minutes after launch
| Pilot | Given | Time, tool calls | Judge | Registered test | Against the hand proof |
|---|---|---|---|---|---|
| 1: hexagon law | the statement | 15 min, 35 | passed, round 1 | 15 of 15 sizes | a different route |
| 2: triangle laws | the statements | 41 min, 40 | passed, round 1 | 40 of 40 predictions | the same route |
| 3: VO + T13's law | a question and data | 53 min, 42 | passed, round 1 | 20 of 20, and the agent's own law 20 of 20 | no proof existed for m = 1 |
| 4: m = 37 | an open question and a census | 95 min, 131 calls; a follow-up took 6 more | passed, round 1 | 180 of 180 claims held at held-out sizes | nobody knew the answer |
| 5: m = 25 | a harder open question, a census and a chance model | 95 min, 108 calls | passed, round 1 5 of 17 explained | 414 of 414 claims held at held-out sizes; our own expectation refuted | nobody knew the answer |
| 6: m = 37 again | a question the fifth pilot's registered test raised | 66 min, 99 calls | passed, round 1 12 of 19 explained | our expectation refuted at 3 of 17 sizes, by exactly the agent's nine rules, where it predicted them | nobody knew the answer |
Pilot 1's agent ran as a subagent in the orchestrator's container; every later agent ran in its own container, which held only the sandbox, and its whole transcript was audited.
What the judge checks
Each check answers a specific way an agent's work could look right and be wrong.
| If the agent… | it is caught by |
|---|---|
| edits the library to make its proof easier | a SHA-256 manifest of every library file, and a diff of its branch against the base commit |
| proves a weaker statement than asked | the target statement, checked again from a pinned copy the agent cannot edit |
leaves a gap, with sorry or a new axiom | #print axioms, which must list only propext, Classical.choice and Quot.sound |
| has a proof that builds only in its own copy | a rebuild against a fresh copy of the real library |
| fits its law to the data it was given | the law, evaluated at held-out sizes; the agent is told the comparison exists, never its result |
| looks the answer up | a container that holds only the sandbox, and an audit of the whole transcript, read from the server, for any step across that boundary |
What the pilots do not show
They show that the loop's mechanics work end to end, with real isolation, and that an agent can carry a technique to a new setting, find an unstated law from data, prove a case nobody had proved, and answer a question nobody had answered. They do not show that the hard questions are within reach. The fourth pilot's mechanism is elementary once seen, and the atlas's own tools could have found its key factor had anyone looked for factors shared between rules. Each library held close worked examples, and the agents said they followed them. The fifth pilot answered only part of its question, and left twelve cases unexplained. The sixth pilot's answer was a factorisation we had listed as unchecked and not tried. Six runs on six problems say little about how often the approach fails, or where it stops working.