Experiments 12
No Goals
Step through interactive proofs checked by Lean 4, or switch to the night shift to watch an agent test and formalize claims around the Riemann hypothesis.
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
A Rust service runs Lean 4.35 through the Lean REPL and replays your proof from the start on each step, with a five-second timeout. The input accepts single core-Lean tactics (rfl, decide, exact, intro, obtain, constructor, left, right, rw, induction, omega) and rejects sorry or native_decide. Progress is saved in local storage.
The night shift
Architecture
Qwen3.5-2B runs on four CPU cores inside a Rust loop built with rig and backed by SurrealDB. A bandit selects the active front: critical-line zeros, argument-principle rectangles, random-matrix statistics, Robin’s inequality, the Mertens function, elliptic curves over finite fields, or Lean formalization.
Verification
Numerical claims must be pre-registered before calling deterministic Rust instruments (Riemann–Siegel with Gabcke bounds and Turing’s method for zeros; the argument principle for off-line rectangles). Results already implied by known bounds earn zero credit. Formal claims are accepted only when Lean 4 checks the exact registered statement against Mathlib using standard axioms (propext, Classical.choice, Quot.sound).