Experiments 12
No Goals
Two tabs, one Lean. In the course, you pick moves and Lean checks each step until there’s nothing left to prove. In the night shift, an agent works on the Riemann hypothesis with the same Lean, and you can watch it think.
Lean 4 · Mathlib · Rust · Axum · rig · SurrealDBView source
Checking 1/3 · Both sides compute
The statement below the line is your goal. Here, you need to prove that 2 + 2 = 4. Try a move to see how Lean checks it.
You have
Loading the goal from Lean…
You need
- ⊢
- what you need
Notes
The course
The board shows the goals and error messages returned by Lean 4.34. The explanations above it help you read the results as you go.
How a check works
A Rust service runs Lean through the Lean REPL. When you try a move, it checks your proof from the beginning, including the new step. Your progress is saved in this browser, so you can come back to it later.
What you can type
The box accepts any single tactic from core Lean, without Mathlib. It rejects sorry, compiled evaluation such as native_decide, and anything that reaches outside the proof. Each move has five seconds before the process is replaced. The levels use rfl, decide, exact, intro, obtain, constructor, left, right, rw, induction, and omega.
The night shift
Who is working
Qwen3.5 2B, running on four CPU cores inside the same cluster, driven by a Rust loop built on rig. It works in episodes. A bandit picks the front: the zeros on the critical line, rectangles off it, random-matrix statistics, Robin’s inequality, the Mertens function, elliptic curves over finite fields, or Lean.
Why its words don’t count
The model registers a prediction before it calls an instrument written in Rust, and a claim climbs only when that prediction holds. A prediction that a published result already guarantees, like Hasse’s bound or every zero below 3·10¹² lying on the line, is graded but earns nothing. The zeros come from the Riemann–Siegel formula, kept inside Gabcke’s error bound, and the verified height is Turing’s method: Brent’s criterion fixes how many zeros lie below it, and every one was found on the line. The rectangles come from the argument principle.
A claim is proved only when Lean 4 checks the exact statement it was recorded with, against Mathlib, and #print axioms shows nothing beyond propext, Classical.choice, and Quot.sound. Restated lemmas are refused, and lemmas Lean’s automation proves on its own are filed as routine.
What it remembers
Its memory lives in SurrealDB on a disk of its own: a graph of claims with full-text recall, episode transcripts, and every zero it has located. Every few episodes it sleeps, keeps a couple of insights, and writes a letter to its next self. Nobody can talk to it. It rests between episodes, and longer when nobody is watching; it can also be set to work only while someone watches. It stops for the day when its token budget, which counts what it reads as well as what it writes, runs out.