Leanstral 1.5: Proof Abundance for All

Mistral's proof-engineering model just got a serious upgrade, and the numbers are hard to ignore. Leanstral 1.5, released under Apache-2.0 with 119B total parameters but only 6B active, now saturates miniF2F entirely — 100% on both validation and test sets — and chews through 587 of 672 PutnamBench problems. On FATE-H and FATE-X, the graduate and PhD-level abstract algebra benchmarks, it posts new state-of-the-art scores of 87% and 34%. Those are competition-math numbers, not toy-problem numbers.

What makes this release interesting isn't just the scores but the price tag behind them. Mistral says Leanstral edges out Seed-Prover 1.5's high setting on PutnamBench by seven problems while costing around $4 per problem, versus an estimated $300-plus for Seed-Prover, which burns through 10 H20-days per problem. Compare that to Aleph Prover's $54-68 per problem, and Leanstral starts looking less like a research curiosity and more like something you could actually run in production. The model also scales its reasoning smoothly as you give it more tokens — solving 44 problems at a 50k budget, climbing to 244 at 200k, 493 at 1M, and topping out at 587 with 4M tokens. No plateau, no giving up. One proof involving AVL tree insertion and deletion complexity ran for 2.7 million tokens across 22 context compactions before Leanstral nailed down a tight O(log n) bound.

The training recipe behind this is a three-stage pipeline: mid-training, supervised fine-tuning, then reinforcement learning using something Mistral calls CISPO. Two RL environments do the heavy lifting. One is a straightforward prove-or-disprove loop where the model gets compiler feedback and iterates until a proof compiles or it runs out of budget. The other treats Leanstral like an actual developer sitting in a repo — editing files, running bash commands, querying the Lean language server for type errors and goal states in real time. That second environment is clearly where the agentic muscle comes from, since it's what lets the model persist through long-horizon tasks instead of choking on a single hard subgoal.

The more striking demonstration, though, is what happens when you point this thing at real code instead of competition math. Mistral built a pipeline using Aeneas to translate Rust into Lean, then had Leanstral infer intent and generate correctness properties, attempting to prove or disprove each one. Run across 57 repositories, it flagged 47 violated properties, 11 of which turned out to be genuine bugs — five previously unreported on GitHub. One was a nasty overflow in the sign function of a zigzag-decoding library, datrs/varinteger, where feeding it Std.U64.MAX caused silent corruption in release builds. That's the kind of edge case fuzzing routinely walks right past.

On the practical side, Mistral also open-sourced FLTEval, a benchmark built from real pull requests to the Fermat's Last Theorem formalization project. Leanstral 1.5 lifts pass@1 there to 28.9 and pass@8 to 43.2, beating Anthropic's Opus 4.6 score of 39.6 at a fraction — Mistral says one-seventh — of the cost. Weights are on Hugging Face, there's a free API endpoint, and Mistral is pushing people toward its Vibe coding agent with an optional Lean LSP MCP server for anyone who wants to point this at their own codebase.