Summary: Mistral released Leanstral 1.5 on July 2, 2026 as a sparse 119B-parameter proof model with Apache 2.0 weights. The company reports that miniF2F is saturated and PutnamBench reaches 587 of 672 at about $4 per Putnam problem. That cost profile makes repeated formal proof searches more practical, although the results come from Mistral’s announcement.
Leanstral 1.5 landed on July 2, 2026, carrying the tagline “Proof abundance for all” — proof treated as abundance, within everyone’s reach. This is the first big overhaul since the original model appeared in March: a sparse Mixture-of-Experts build that holds 119B total parameters yet wakes only about 6B of them per token, with the weights fully published under Apache-2.0. Over on Hugging Face, the model card mistralai/Leanstral-1.5-119B-A6B states a 256k context window (200k recommended), and the leanstral-1-5 API endpoint is free of charge for the time being.
How big is the jump? Read the scores. On single-sample FLTEval, the March original managed 21.9; version 1.5 lifts pass@1 to 28.9 and takes pass@8 from 31.9 up to 43.2, clearing Claude Opus 4.6’s 39.6 while spending roughly one-seventh as much. miniF2F matters even more: every problem in the validation and test sets has now been solved, so the standard benchmark for Lean 4 proof engineering is officially saturated.
Where 1.5 Diverges
The skeleton is the original’s sparse design; this revision pours its energy into training and environments. Deployment is business as usual: host the weights yourself, call the free API, or get it running with vibe --agent lean inside Mistral Vibe. The model card bills it as a straight upgrade of the original Leanstral-2603 — text and image in, text out — but the arena it competes in is exactly one: proof engineering in Lean 4. For formal-verification teams it is still the only open-weights tool in this class that installs and runs on hardware you own. Mistral sells it as a specialist, not a general coding model: a deliberately narrow scope with efficiency pushed hard.
A Three-Stage Pipeline, Two RL Settings
Training moved through three stages: mid-training, then supervised fine-tuning, and finally reinforcement learning driven by the CISPO algorithm. That RL ran in two settings. The first, “multiturn proving”: the model attempts to prove or disprove theorems, adjusting against Lean compiler feedback until it either lands the result or runs the budget dry. The second, a “code agent”: the model operates on a raw filesystem the way a developer does — editing files, running bash, talking to the Lean language server — on long-horizon jobs such as filling in the missing proofs of a partial repository, with Mistral’s in-house fork of SafeVerify ruling on correctness. Together the two settings track how genuine proof work unfolds: short loops against the compiler, then marathon sessions at repository scale.
The Scoreboard: Full Marks on miniF2F, 587 on PutnamBench
Lay the numbers out. miniF2F: 100% on validation and test alike. PutnamBench: 587 of 672 problems down. FATE-H: 87 problems (87%); FATE-X: 34 problems (34%) — each benchmark’s previous best rewritten. The test-time scaling curve holds up just as cleanly: on PutnamBench, pass@8 moves from 44 problems at 50k tokens to 244 at 200k, 493 at 1M, and 587 at 4M, climbing monotonically with no premature flattening. Mistral shipped FLTEval itself as open source alongside the model, so the next round of comparisons can share a single ruler. Set against March, no earlier generation moved these suites by this much for the company.
Four Dollars a Problem: The Cost Math
Cost is the most striking figure in the announcement: Leanstral 1.5 clears a PutnamBench problem at about $4 apiece. And the rest of the field? Seed-Prover 1.5 at its high-intensity setting is estimated to burn more than $300 per problem (around 10 H20-days of compute each), while Aleph Prover lands between $54 and $68. This is not a percentage gap; it is a chasm of one to two orders of magnitude. On Mistral’s pricing, sweeping all of PutnamBench costs less than a few frontier-model attempts elsewhere. The sparse design is the product logic in plain sight: proof search feeds on massive parallel sampling, and pass@k only becomes playable once a single roll is cheap. For verification teams, that is the divide between “try it once” and “run it all day.”
Beyond Proofs: Hunting Real Bugs
Two case studies deserve a record. First: handed a real-world AVL tree implementation, the model fully proved the O(log n) time complexity of insertion and deletion — the run consumed more than 2.7M tokens and 22 context compactions, closing with a bound of 48 steps per height unit plus a constant, nearly as tight as such bounds get. Second: wiring Aeneas (a translator that turns Rust into Lean) into a pipeline with Leanstral scanned 57 repositories and flagged 47 violated properties, 11 of them genuine bugs and 5 never reported before — among them an integer overflow in the zigzag-decoding sign function of datrs/varinteger at Std.U64.MAX. A proof model catching bugs that humans overlooked comes closer to the “proof abundance” promise than any scoreboard.