Mistral's Open-Source Leanstral 1.5 Aces Formal Math Benchmarks — and Finds Five Real Bugs

Mistral AI has released Leanstral 1.5, an open-weights model purpose-built for formal software verification, that both tops the hardest theorem-proving benchmarks and — more consequentially — surfaced five previously unknown bugs in real-world code during testing. It is a rare demonstration of AI moving from "solves math puzzles" to "catches errors humans missed."

The Model

Leanstral 1.5 is released under the permissive Apache 2.0 license, with 119 billion total parameters and only about 6.5 billion active per inference — a mixture-of-experts design with 128 experts, four active per token, and a 256,000-token context window. It targets Lean 4, the proof assistant increasingly used to write machine-checkable mathematical proofs and to formally verify that software behaves exactly as specified.

Trained through a pipeline of mid-training, supervised fine-tuning, and reinforcement learning with the CISPO method, the model is optimized for agentic proof engineering — iteratively constructing, checking, and repairing proofs rather than producing them in a single shot.

The Benchmarks

The results are striking. Leanstral 1.5 saturates miniF2F, the standard olympiad-level formal-math benchmark; solves 587 of 672 problems on PutnamBench, drawn from the notoriously difficult Putnam competition; and posts state-of-the-art scores on the FATE benchmark suite, reaching 87% on FATE-H and 34% on FATE-X.

These are not incremental gains. Formal theorem proving has been one of the slowest domains for AI progress precisely because it admits no bluffing — a proof either type-checks or it doesn't. Saturating miniF2F means the community will need harder benchmarks to measure the next generation.

From Proofs to Bugs

The headline for practitioners isn't the benchmark sweep — it's what happened when Leanstral 1.5 was pointed at real code. Across 57 repositories tested, the model uncovered five previously unknown bugs, demonstrating agentic proof engineering applied to actual software verification rather than contrived exercises.

That capability matters because formal verification has long been gated by cost: writing machine-checked specifications and proofs is painstaking expert work, which is why it's largely confined to safety-critical systems like avionics, chip design, and cryptographic protocols. A capable open model that can do the grunt work of proof construction lowers that barrier, potentially bringing formal guarantees to far more software.

Open, and Aimed at a Frontier

By releasing Leanstral 1.5 open-weight and free via a public API, Mistral plants a flag in a domain the frontier labs have largely left open. It also fits a broader movement: mathematicians at Imperial College London are using autoformalization tools to encode Fermat's Last Theorem into Lean, and the formalized proofs generated by projects like Leanstral's benchmarks become high-quality training data for the next round of mathematical AI.

The trajectory points toward a future where "prove it" becomes a literal, automated demand — where AI doesn't just write code, but produces machine-checkable evidence that the code does what it claims. Leanstral 1.5 is one of the clearest signposts yet that the future is arriving in the open.