On July 2, 2026, Mistral released Leanstral 1.5 under the tagline “Proof abundance for all.” It is the first major revision since the original model landed in March: 119B total parameters with only about 6B active per token in a sparse Mixture-of-Experts design, weights fully open under Apache-2.0. The Hugging Face model card mistralai/Leanstral-1.5-119B-A6B lists a 256k context window (200k recommended), and the API endpoint leanstral-1-5 is free for now.
The leap is written in the scores. The original Leanstral scored 21.9 on single-sample FLTEval in March; 1.5 pushes pass@1 to 28.9 and pass@8 from 31.9 to 43.2 — past Claude Opus 4.6’s 39.6 at roughly one-seventh the cost. And on miniF2F, the standard benchmark for Lean 4 proof engineering, the model now solves every problem in both the validation and test sets. Saturated.
What Changed in 1.5
The architecture carries over the original sparse design; the revision is all about training and environments. Deployment paths are unchanged: self-host the weights, call the free API, or launch with vibe --agent lean inside Mistral Vibe. The model card positions it as a direct upgrade of the original Leanstral-2603, accepting text and image input and producing text output — but its battlefield is exactly one: proof engineering in Lean 4. For formal-verification teams, it remains the only open-weights tool in this class you can install and run on your own hardware. Mistral pitches this not as a general coding model but as a specialist: narrow scope, aggressive efficiency.
Three Training Stages, Two Environments
Training ran in three stages: mid-training, supervised fine-tuning, then reinforcement learning with the CISPO algorithm. RL played out in two environments. The first is “multiturn proving”: the model proves or disproves theorems, iterating against Lean compiler feedback until it succeeds or exhausts its budget. The second is a “code agent”: the model works a raw filesystem like a developer — editing files, running bash, calling the Lean language server — on long-horizon tasks such as completing the proofs of a partial repository, with correctness checked by Mistral’s own fork of SafeVerify. The two environments mirror how real proof work happens: quick iterations against the compiler, and long repo-scale sessions.
Benchmarks: miniF2F Saturated, PutnamBench at 587
The numbers. miniF2F: 100% on both the validation and test sets. PutnamBench: 587 of 672 problems solved. FATE-H: 87 problems (87%) and FATE-X: 34 problems (34%), both new records for those benchmarks. The test-time scaling curve is just as clean: pass@8 on PutnamBench climbs from 44 problems at 50k tokens to 244 at 200k, 493 at 1M, and 587 at 4M — monotonically, with no early plateau. Mistral also open-sourced FLTEval itself alongside the release, so the next round of comparisons has a shared ruler. Against the March numbers, this is the largest single-generation gain the company has posted on any of these suites.
The $4-a-Problem Economics
The cost figure is the sharpest one in the post: Leanstral 1.5 solves a PutnamBench problem for roughly $4. The comparison set? Seed-Prover 1.5 in its high setting is estimated at over $300 per problem (about 10 H20-days of compute each), and Aleph Prover runs $54 to $68. That is not a percentage gap; it is one to two orders of magnitude. At Mistral’s rate, an entire PutnamBench sweep costs less than a handful of frontier-model attempts elsewhere. The sparse design is the product logic: proof search lives on massive parallel sampling, and pass@k is only playable when a single roll is cheap. For verification teams, this is the line between “try it once” and “run it all day.”
From Proving to Bug Hunting
Two case studies are worth recording. First, against a real AVL tree implementation, the model fully proved O(log n) time complexity for insertion and deletion: over 2.7M tokens and 22 context compactions, ending in an almost tight bound of 48 steps per height unit plus a constant. Second, pairing Aeneas (a Rust-to-Lean translator) with Leanstral into one pipeline scanned 57 repositories and flagged 47 violated properties — 11 genuine bugs, 5 of them never previously reported — including an integer overflow in the zigzag-decoding sign function of datrs/varinteger on Std.U64.MAX. A proof model catching bugs humans missed is the part of this release closest to the “proof abundance” promise.
Sources
- Leanstral 1.5: Proof abundance for all — Mistral AI
- Leanstral-1.5-119B-A6B model card — Hugging Face
- Leanstral 1.5 discussion — Hacker News
AI-assisted summary compiled from the sources above, reviewed by a human before publishing.