Leanstral 1.5 has been released, promising to make proof abundance accessible to everyone. This update likely introduces new features or improvements to assist in formal proof development.
SynthePulse Insight · AI deep reading
Version 1 · 2 sources
Mistral AI releases Leanstral 1.5, which matches or surpasses closed-source models on formal mathematics benchmarks with only 6B active parameters, and discovers unknown bugs in real codebases, demonstrating the practical potential of open-source formal verification.
Leanstral 1.5 achieves remarkable results on multiple formal mathematics benchmarks. According to Mistral AI's official blog, the model reaches 100% on miniF2F (both validation and test sets), solves 587/672 problems on PutnamBench, and achieves new state-of-the-art results of 87% and 34% on FATE-H and FATE-X, respectively. These benchmarks cover mathematical problems ranging from high school to PhD level.
Compared to existing models, Leanstral 1.5 solves 7 more problems on PutnamBench than Seed-Prover 1.5 (high setting), but at a significantly lower cost: about $4 per problem versus an estimated $300+ for Seed-Prover. The closed-source model Aleph Prover costs $54-68 per problem but ranks higher.
In terms of test-time scaling, as the token budget increases from 50k to 4M, the number of PutnamBench problems solved monotonically rises from 44 to 587, demonstrating the model's sustained capability in long reasoning chains.
Leanstral 1.5 employs a three-stage training process: intermediate training, supervised fine-tuning, and CISPO-based reinforcement learning. Training occurs in two RL environments: a multi-turn environment where the model submits proofs and receives feedback from the Lean compiler, and a code-agent environment where the model edits files, runs bash commands, and uses the Lean language server to check goals in real time, similar to a developer.
The code-agent environment enables the model to handle long-horizon tasks, such as completing partial proofs, building auxiliary lemmas, and working continuously through multiple context compactions. Correctness is ultimately verified through SafeVerify's branch verification.
The model has 119B total parameters but only 6B active parameters, and is fully open-sourced under the Apache-2.0 license.
Although primarily trained for mathematics, Leanstral 1.5 excels at code verification. In tests across 57 open-source repositories, it discovered 5 previously unknown bugs, including an overflow issue in the Rust library varinteger.
A case study demonstrates an AVL tree time complexity proof: the model used over 2.7 million tokens and 22 compactions, employing structural induction and monadic time tracking to prove the O(log n) height guarantee for a real implementation.
On the FLTEval benchmark, pass@1 improved from 21.9 to 28.9, and pass@8 from 31.9 to 43.2, surpassing Opus 4.6's 39.6, at only one-seventh the cost.
Leanstral 1.5 is available via Hugging Face and a free API, and the FLTEval benchmark is open-sourced. This lowers the barrier to formal verification, allowing researchers and developers to use it for free.
Mistral AI emphasizes that the model strikes a balance between openness and practicality, making rigorous formal methods effective and practical in real-world scenarios.
This report is primarily based on Mistral AI's official blog and secondary reporting from THE DECODER. All benchmark data, cost estimates, and bug discoveries are from official statements and have not been independently verified. Cost comparisons (such as Seed-Prover's $300) are official estimates and may vary depending on hardware and configuration.
Leanstral 1.5, with its extremely low active parameter count and open-source license, matches or surpasses closed-source models in formal mathematics and code verification, demonstrating the practical potential of open-source formal verification. However, its performance data relies primarily on official reports.
Primary report
Primary source
Also covered by 1 sources