Mistral AI has released Leanstral 1.5, an open-source model built to write and check formal proofs in Lean 4. It’s a specialized tool with a specific job: Verifying that mathematical reasoning and code logic are actually correct, not just plausible.
The numbers are the headline. Mistral says the model hits 100% on miniF2F, a formal math benchmark that spans high school problems up through olympiad difficulty. On PutnamBench, a set of 672 problems from the Putnam math competition, Leanstral 1.5 solved 587 of them. On two harder algebra benchmarks, FATE-H and FATE-X, which test graduate- and doctoral-level work in areas such as group theory and ring theory, it posted top open-source scores of 87% and 34%, respectively. Only one closed-source competitor, Aleph Prover, beats it on PutnamBench.
The model is released under the Apache 2.0 license, so developers can use, modify, and deploy it without the licensing restrictions that come with many frontier models. It runs as an 119-billion-parameter mixture-of-experts model, but only about 6 billion parameters are active at once. That keeps inference costs down relative to its size.
Why Lean 4 Matters Outside of Math Contests
Lean 4 is a proof assistant. In plain terms, it’s software that checks whether a mathematical argument holds up, step by step, with no room for hand-waving. That kind of rigor has obvious value for pure math research. It also has a practical use for engineering teams: Formal verification of code.
Lean 4 is already used in formal mathematics and software verification, and some teams rely on proof systems to check code that can’t afford to fail. Chip design, safety-critical software, security-sensitive systems — the kind of places where a small logic error causes a very expensive failure. A model that can work in that world, at a fraction of the cost of prior approaches, changes who can afford to use it.
Mistral is backing that claim with a real example. Beyond the benchmark scores, Leanstral 1.5 has already found five previously unknown bugs while scanning 57 open-source repositories. That’s a different kind of proof point than a leaderboard score. It suggests the model can be pointed at existing codebases and catch problems that human reviewers missed.
How it Actually Works
Leanstral operates as a code agent inside a raw filesystem. It edits files, runs bash commands, and communicates directly with the Lean language server, which provides it with goals, errors, and type information in real time. That setup lets the model work incrementally: complete partial proofs, build supporting lemmas, and keep going even when a task runs long enough to require compacting its own context window.
That last part matters more than it sounds. Mistral says the model handled one case involving more than 2.7 million tokens across 22 separate context compactions while proving a time-complexity guarantee for an AVL tree. That’s not a quick answer. That’s a model working through a hard problem over a long session.
Mistral also built in a way to trade cost for accuracy. Results on PutnamBench improved along a clear curve as the team raised the token budget per attempt: 44 problems solved at a 50,000-token budget, 244 at 200,000 tokens, 493 at 1 million tokens, and the full 587 at 4 million tokens. That gives teams a real lever. Need a fast answer? You get one. Need the model to actually finish the proof? Let it run longer.
Training occurred in three stages: Mid-training, supervised fine-tuning, and reinforcement learning using the CISPO method. During the reinforcement learning phase, the model operates in a loop — it submits a proof to the Lean compiler, receives feedback on whether it compiles, and revises until it succeeds or the loop ends. That feedback loop is a big reason the model can push through long, difficult proofs instead of stalling out.
What This Means for DevOps Teams
Mitch Ashley, VP and practice lead for software lifecycle engineering and AI-native software engineering at The Futurum Group, says the release marks a real shift for a specific slice of the software lifecycle. “Machine-checkable correctness enters the software lifecycle for the code that cannot afford to fail,” Ashley said. “A model that generates proofs, a compiler that validates changes the economics of formal verification, a practice most teams skipped as too slow and too specialized.”
Ashley also points to a question this approach answers that many AI tools don’t. “The harder question is what checks the checker when both run at machine speed,” he said. “Formal verification answers it because the final arbiter is a compiler, not another model. Teams that let one model review another trust a watcher that nothing verifies.”
That distinction matters. Many AI code review tools have one model checking another model’s work, with no independent ground truth. Leanstral’s proofs get validated by a compiler, not by a second opinion from another language model. That’s a meaningfully different trust model.
This isn’t Mistral’s first attempt here, either. The company’s March 2026 Leanstral release reportedly outperformed Claude Sonnet by 8 points at pass@16 while costing 15 times less to run. Leanstral 1.5 builds on that work rather than starting over.
The model supports a 256,000-token context window and is available at no cost through Mistral’s Labs tier via the console playground, as well as via Hugging Face weights and local deployment with vLLM. For teams already experimenting with AI-assisted code verification, that low barrier to entry is worth a look.
