2026-07-03 · 8 min · agents · reinforcement-learning · formal-methods
Why read this
Nichelast 15%Explains how Leanstral proves Lean theorems with a plain code-agent loop, why accuracy scales with token budget, and how SafeVerify blocks reward hacks.
- A new technique
- Open code or weights
- Explained from first principles
Agents & harnessesNeeds a workstation GPUApache-2.0Practitioner model
How this was scored
- Is it new?
- 2 of 3: A real new idea, method or capability
- Can I trust it?
- 0 of 3: Restates claims
- Can I run it?
- 2 of 3: Open code or weights with real limits
- Will I understand it?
- 2 of 3: Mechanism from first principles with figures
- Can I act on it?
- 1 of 3: General advice
- Will it last?
- 1 of 3: Relevant for months
- Does it affect many?
- 1 of 3: A specialist community
- Only here?
- 0 of 3: Same as the press release
Score 38 of 100, ranked 540 of 577 rated articles. Each question is answered 0–3 by hand, and a 3 is rare. How articles are scored
Formal theorem proving is the rare corner of ML where correctness is not a vibe: a proof either type-checks against Lean's kernel or it doesn't. The catch is that the strongest Lean systems tend to win with machinery around the model — Seed-Prover runs conjecture proposing and lemma pools at a budget of ~10 H20-days per problem; Goedel-Architect generates a blueprint and proves lemmas in parallel. Powerful, but none of it is the interface a person actually uses to write Lean.
Mistral's Leanstral 1.5 makes the opposite bet. It's a 119B-parameter Mixture-of-Experts that activates just 6B per token, and it proves theorems by doing exactly what a developer does in Mistral Vibe: edit files, run shell commands, and query the Lean language server for goals, types, and errors — then revise, and keep going. No prover scaffold. Its test-time scaling is nothing more exotic than running that loop longer. And it works: it saturates miniF2F (100% on validation and test), solves 587/672 PutnamBench, and sets a new open state-of-the-art of 87 on FATE-H and 34 on FATE-X — while being Apache-2.0.
The loop is the whole method
There's no separate "prover mode." A theorem — or a repository with a missing proof — enters the same agent harness used for ordinary software engineering, and the model works it turn by turn:
Mistral's own diagram of the loop shows the same thing at the token level: the system prompt hands the
model lean-lsp-mcp tools, and from there it's assistant turns interleaving <think>, tool calls, and
tool results — the agent editing a Lean file and checking it exactly as it would edit and test any other
codebase, through Vibe's raw filesystem / bash / MCP surface.
Why insist on the ordinary loop? Two reasons. It makes the model usable — you point it at a Lean repo the way you'd point a coding assistant at any repo — and, more importantly, it means the model is trained in the same long-horizon interaction pattern it uses at inference. There's no train/test interface gap to paper over.
Test-time scaling, without a trick
Because the model just spends tokens inside that loop, its accuracy is a smooth function of the per-attempt token budget. This is the headline result, and it's worth playing with — drag the budget and watch PutnamBench solved climb:
That monotonic climb — 44 solved at 50k tokens, 244 at 200k, 493 at 1M, 587 at 4M — is Leanstral's whole argument in one curve. Rather than giving up when a proof runs long, it keeps reasoning, editing, and compacting context, turning budget directly into solved theorems. Here's Mistral's version of the same figure:
The economics are the striking part. On PutnamBench, Leanstral edges Seed-Prover 1.5's high setting by 7 problems (587 vs 580) at roughly $4 per problem against an estimated $300+ for Seed-Prover, whose high setting budgets ~10 H20-days per problem. The only systems above it run under different rules — natural-language proof guidance, or a much larger cost like Aleph Prover at $54–68 per problem.
Why you can't fake a proof
Turning compiler feedback into an RL reward is dangerous: if the objective is just "make Lean stop
complaining," the cheapest policies are to cheat — leave a sorry, call the unsound native_decide,
assume an extra axiom, or loosen the checker with set_option. Leanstral is graded by a fork of
SafeVerify, which is built to reject every one of those. Full reward requires a proof that compiles,
uses only standard Lean axioms (checked via #print axioms), and took no shortcut. Toggle the cheats
and watch the verdict flip:
This adversarial verifier is what makes the reinforcement learning honest. Leanstral trains on two RL environments through a CISPO objective: a multiturn environment where it must prove or disprove a theorem, getting Lean compiler feedback between attempts until it succeeds or runs out of budget; and a code-agent environment where it acts as a developer across a whole repository. Mistral's diagram of the multiturn loop is the picture of a verifier-gated reward — the same instinct as Agents-A1's verifier-graded RL, specialized to Lean:
The numbers
On competition math, Leanstral is the best open result across the board — the caveat being that a couple of systems above it on PutnamBench either use natural-language guidance or cost 10–75× more to run:
The result that best captures the "keep working the problem" behaviour is FLTEval — proof-engineering tasks drawn from real pull requests to the Fermat's Last Theorem repository. Here Leanstral 1.5 tops even frontier general models, at a fraction of the cost:
Mistral's own charts show the full comparison set — the three-benchmark bar chart (PutnamBench / FATE-H / FATE-X) and the FLTEval scaling across pass@1/2/4, where 1.5 pulls clearly ahead of much larger open models:
It generalizes past math
Because the skill it learned is proof engineering in a repository, not competition-problem pattern matching, it transfers to code verification:
- AVL trees. Leanstral proved the
O(log n)time-complexity guarantees for a real self-balancing-tree implementation — structural induction mirroring the recursion, unfolding aTimeMmonad to expose the step counts, exhaustive rebalancing-case analysis. It ran over 2.7 million tokens across 22 context compactions to close it: the test-time-scaling curve in practice. - Finding real bugs. In an automated pipeline — Aeneas translates Rust to Lean, Leanstral infers the
intended properties and tries to prove each (or disprove it) — across 57 repositories it flagged 47
violated properties, 11 genuine bugs, 5 previously unreported. One was an integer overflow in
datrs/varinteger's zigzag decode: onU64.MAX,value + 1overflows — a crash in debug, silent corruption in release, exactly the edge case fuzzing tends to miss.
The take
Leanstral's contribution isn't a clever proof-search algorithm; it's a stance. The formal-proving leaderboard has been climbing by wrapping models in ever-more-specialized test-time scaffolds, and Leanstral shows that a plain code agent — trained in the loop it's evaluated in, graded by a verifier it can't cheat — matches or beats that machinery at a fraction of the cost, while staying usable by anyone who can drive a coding assistant. The MoE is efficient (6B active), the license is open (Apache-2.0), and the scaling story is the honest kind: no plateau trick, just compute converted into checked proofs. The open question is how far "just run the agent longer" goes as problems get genuinely harder than Putnam — but as a demonstration that formal verification can be practical infrastructure rather than a prover-lab specialty, it's the most encouraging Lean release in a while.
Built on the Leanstral technical report and Mistral's Leanstral 1.5 announcement (Mistral AI, 2026; Apache-2.0, weights on Hugging Face). Figures are reproduced from Mistral's report and blog post; benchmark and cost figures are quoted from those sources.