Mistral AI shipped Leanstral 1.5 on July 2, an update to its open Lean 4 proof engineering model. The blog post lays out the headline numbers: a saturated miniF2F, 587 of 672 PutnamBench problems solved, and new highs on two graduate algebra benchmarks. Weights are on Hugging Face under Apache 2.0, with a free API endpoint.
What Lean 4 actually does
Lean 4 is a proof assistant. You write a mathematical claim or a property of some code, and the compiler either accepts the proof as correct or it doesn't. There's no bluffing. A model that sounds convincing but writes a wrong proof gets rejected by the compiler, which is the whole point and why this niche keeps drawing attention.
Leanstral 1.5 didn't change shape from the version Mistral put out in March. Same mixture-of-experts setup, 119 billion total parameters with roughly 6 billion active, 256k context, image input. What changed is the training. The model now runs through mid-training, supervised fine-tuning, and reinforcement learning with CISPO, across two environments: one where it argues proofs back and forth with the Lean compiler, and one where it behaves like a developer editing files in a real repository.
The benchmark numbers, and what they leave out
The miniF2F result is 100 percent on both validation and test sets. Saturating a benchmark tends to mean the benchmark is done being useful, not that the problem is solved, and some readers online were quick to call the whole release benchmaxxed. Take that as you will.
PutnamBench is the more interesting line. Leanstral 1.5 solves 587 of 672 problems, edging out Seed-Prover 1.5 at its high setting by seven problems. The cost gap is where Mistral clearly wants your eye: about $4 per problem against an estimated $300 or more for Seed-Prover, whose high setting burns a budget of 10 H20-days per problem. That's Mistral's estimate of a competitor's cost, not an audited figure, so treat the 75x framing accordingly. Still, a 6B-active model getting there at all is the story.
On the FATE-H and FATE-X algebra sets, Mistral reports 87 and 34 problems respectively and calls both state-of-the-art. The company also notes that provers ranked above it on PutnamBench run under different conditions, some with natural-language proof guidance, some far more expensive. Worth reading that caveat before you treat any single leaderboard position as settled.
Catching bugs in real Rust
The part that reaches past pure math: Mistral built a pipeline that translates Rust to Lean, has Leanstral guess the intended correctness properties, then tries to prove them. Across 57 repositories it flagged 47 violated properties. Eleven of those were genuine bugs. Five had never been reported on GitHub.
One was an integer overflow in the sign function of a varint decoding library, where adding one to the maximum U64 value crashed in debug and silently corrupted data in release. The kind of edge case fuzzing usually walks right past. The SafeVerify fork handles the correctness checking, and Mistral open-sourced its FLTEval benchmark alongside the release.
The March version was pulled when 1.5 landed. Leanstral 1.5 is available now as leanstral-1-5 through the free API, with Mistral recommending its Vibe agent for actually running it.
