Mistral Releases Leanstral 1.5, an Open Model for Formal Proof and Code Verification
Mistral released Leanstral 1.5, a free, open model that saturates a major proof benchmark and found 5 unknown bugs while checking real code.
What shipped
Mistral released Leanstral 1.5, a free, Apache-2.0 licensed model with 119B total parameters but only 6B active parameters, built to make formal verification in Lean 4 "more powerful and accessible than ever." The model reaches 100% on both the validation and test sets of miniF2F, a cross-system benchmark for formal mathematics spanning elementary problems through IMO-level challenges. On PutnamBench, a set of 672 problems drawn from the Putnam Mathematical Competition, Leanstral 1.5 solves 587 of them. On two abstract-algebra benchmarks for graduate and PhD-level problems, FATE-H and FATE-X, it reaches new state-of-the-art marks of 87% and 34% respectively.
How it was trained
Leanstral 1.5 goes through mid-training, supervised fine-tuning, and reinforcement learning using a method Mistral calls CISPO. Training leans on two reinforcement-learning environments. In the multiturn environment, the model is given a theorem statement, submits a proof, receives compiler feedback from Lean, and keeps refining until the proof compiles or its budget runs out. In the code agent environment, the model behaves like a developer working in a raw filesystem: it edits files, runs bash commands, and uses the Lean language server to inspect goals, errors, and type information, letting it work through long tasks such as completing partial proofs across many rounds of context compaction.
Cost and scaling
On PutnamBench, Mistral compared Leanstral 1.5 against Goedel-Architect without natural-language guidance, Seed-Prover 1.5 at its high setting, and AxProverBase, and says it edges out Seed-Prover 1.5's high setting by 7 problems at roughly $4 per problem, against an estimated $300 or more for Seed-Prover, whose high setting runs on a budget of 10 H20-days per problem. Mistral also reports what it calls the strongest test-time scaling it has seen from a formal-reasoning model: on PutnamBench, Pass@8 climbs from 44 problems solved at a 50k token budget to 244 at 200k, 493 at 1M, and 587 at a 4M token budget. One proof, covering the time complexity of AVL trees, ran for over 2.7 million tokens across 22 compactions.
Finding real bugs
Mistral also fully open-sourced FLTEval, a benchmark built from real pull requests in the Fermat's Last Theorem repository. Leanstral 1.5 lifts pass@1 on that benchmark from 21.9 to 28.9 and pass@8 from 31.9 to 43.2, which Mistral says surpasses Opus 4.6's 39.6 at one-seventh the cost. To test bug-catching ability, Mistral built a pipeline where a tool called Aeneas translates Rust code to Lean, Leanstral infers intended behavior and writes correctness properties, then tries to prove or disprove each one across four attempts per direction. Across 57 tested repositories, the pipeline flagged 47 violated properties, and 11 of those pointed to genuine bugs, 5 of them previously unreported on GitHub. One example: a sign-function bug in the zigzag decoding of the datrs/varinteger library, where the expression "(value + 1)" overflowed on input Std.U64.MAX, causing crashes in debug mode and silent corruption in release mode.
Key facts
- Leanstral 1.5 is a free, Apache-2.0 licensed model with 119B total and 6B active parameters, available on Hugging Face and as a free API called leanstral-1-5.
- It saturates miniF2F (100% on validation and test), solves 587 of 672 PutnamBench problems, and hits 87% on FATE-H and 34% on FATE-X.
- It solves PutnamBench problems at about $4 each, versus an estimated $300 or more per problem for Seed-Prover's high setting.
- Testing across 57 repositories flagged 47 violated properties, 11 of them genuine bugs, 5 of them previously unreported on GitHub.
- Mistral recommends running it through its Mistral Vibe agent tool, optionally paired with a Lean LSP MCP server.
Check your understanding
- How many of the 672 PutnamBench problems did Leanstral 1.5 solve, and roughly what did each solved problem cost?
- Out of 57 tested repositories, how many violated properties did the bug-hunting pipeline flag, and how many turned out to be genuine, previously unreported bugs?