Mistral Ships Leanstral 1.5: 587/672 PutnamBench, 87% FATE-H, 5 Real Bugs Found in Open-Source Repos
Mistral released Leanstral 1.5 today under Apache 2.0, a 119B total parameter MoE model with 6B active parameters built for formal proof engineering in Lean 4. The results move the needle on what open-weight models can do in formal mathematics and real software verification.
Benchmark Numbers
| Benchmark | Score |
|---|---|
| miniF2F | Saturated |
| PutnamBench | 587/672 (87.4%) |
| FATE-H (graduate algebra) | 87% |
| FATE-X (PhD-level algebra) | 34% |
PutnamBench consists of 672 problems from the Putnam Mathematical Competition, which requires deep reasoning and long proof chains. Leanstral 1.5 solves more than four in five. FATE-H and FATE-X are abstract algebra benchmarks testing group theory, ring theory, and module theory at graduate and PhD level respectively.
How It Was Trained
Three stages: mid-training, supervised fine-tuning, and reinforcement learning using CISPO (a variant of GRPO). The model trained on two RL environments simultaneously.
The first is a standard multiturn prover loop: the model gets a theorem statement, submits a proof, receives Lean compiler feedback, and iterates until success or budget exhaustion. The second environment is more consequential: a code agent setup where Leanstral operates in a raw filesystem, editing files, running bash commands, and using the Lean language server to inspect goals and type information in real time. This allows it to work through long-horizon proof engineering tasks across multi-file repositories.
Correctness is verified via Mistral’s fork of SafeVerify, checking against a list of target theorems.
Real Bugs, Not Benchmark Bugs
The practical test: Leanstral 1.5 was run against 57 open-source repositories in agentic mode. It found five previously unknown bugs. These are not evaluation artifacts. They are actual defects in production code that had gone undetected.
That number is modest compared to what Mythos found in curl (one real bug out of a full security sweep). But the comparison isn’t fair: Leanstral is working through formal verification, producing machine-checkable proofs alongside its findings. The mechanism for finding bugs is structurally different from fuzzing or static analysis.
Model Architecture and Access
The 119B total / 6B active ratio reflects a highly sparse MoE architecture. The model is fully open-sourced on Hugging Face and available via a free Mistral API. Apache 2.0 license means unrestricted commercial use.
Context
Formal verification has historically been the domain of specialist researchers working with proof assistants like Isabelle, Coq, or Lean. The appeal of training a model specifically on Lean 4 is that Lean’s type checker provides a ground-truth signal for RL: a proof either compiles or it doesn’t. This binary feedback loop is cleaner than the judgment-based training signals used for most LLM capability areas.
The LEAP paper in April showed GPT-5.5 could solve all 12 Putnam 2025 problems using a general agentic framework. Leanstral 1.5 demonstrates that a 6B-active-parameter specialist can approach those results as a deployable open model running on a fraction of the compute.