No Goals

Back when I was getting my math degree, I remember we covered LaTeX, but there was no mention of Lean. Maybe because it was still “sorta new.” The project started in 2013, with its first official release following in 2014. I wish we’d at least been introduced to it.

I was reading about how AI "proved" the Navier-Stokes equations and I wondered how on earth can you have such an unverifiable thing using AI... I dug deep and wanted to learn about Lean a bit more... as any good mathematician will tell you... practice makes perfect.

That’s the starting point for No Goals. It has two parts: a small course where you work through proofs yourself, and a night shift where an agent "investigates" the Riemann hypothesis.

The course gives you the basics of the environment. The agent is the experiment.

The course

There are nine levels, starting with arithmetic and moving through logic and induction. Each move is a Lean tactic. A Rust service sends your proof, including the new step, to the Lean REPL and returns the goals and errors.

For example:

example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by
  obtain ⟨hp, hq⟩ := h
  constructor
  · exact hq
  · exact hp

When nothing remains, Lean reports “no goals.”

The course uses core Lean without Mathlib. Each move has a five-second limit... check the code out on my github.

The night shift

The agent runs Qwen3.5 2B on four CPU cores, driven by a Rust loop built on rig. It works in bounded episodes rather than one conversation that keeps growing indefinitely because I can't afford running it on frontier models...

A bandit scheduler chooses which area to investigate: zeros on the critical line, regions off it, random-matrix statistics, Robin’s inequality, the Mertens function, elliptic curves over finite fields, or formal proofs in Lean.

The scheduler balances areas that have produced useful results with areas that haven’t been explored much. There’s also a rule that brings the agent back to formal proof work regularly.

During an episode, the agent retrieves relevant memory, sets an objective and prediction, calls tools, reads their results, and records what it learned. Those tools include numerical instruments written in Rust and a Lean workbench with Mathlib loaded.

The important implementation detail is how claims get checked.

Before using a numerical instrument, the model registers a prediction. The tool evaluates it, and the result becomes evidence attached to the claim. Predictions already guaranteed by published results don’t earn credit for discovery.

Numerical evidence also doesn’t turn a conjecture into a theorem. Checking a finite range of zeros can establish something about that range; it doesn’t establish the Riemann hypothesis.

For a formal claim, the agent has to submit a proof of the exact statement recorded in memory. Lean checks it, and the service inspects its dependencies with: #print axioms theorem_name

Lean’s kernel checks the proof terms produced by tactics. The model supplies candidates; acceptance comes from the checker.

Why on earth...

I firmly believe this is the most inelegant way to prove or just do any math... but I just wanted to play around with lean.. I wish the night agent never makes an material progress but I will do secretly root for it.. just a teeny tiny bit.