# Leanstral: proving theorems by being a code agent, not a prover
> Satyajit Ghana — Head of Engineering @ Inkers Technology
> canonical: https://ai.thesatyajit.com/articles/leanstral-formal-proofs
> date: 2026-07-03
> tags: llm, agents, reinforcement-learning, formal-methods, explainer
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](https://mistral.ai): 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 ``, 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](/articles/agents-a1), 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 a `TimeM` monad 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: on `U64.MAX`, `value + 1` overflows — 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](https://github.com/mistralai/LeanstralSafeVerify/blob/main/LeanstralReport.pdf)
and [Mistral's Leanstral 1.5 announcement](https://mistral.ai/news/leanstral-1-5/) (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.*