Leanstral 1.5: Proof Abundance for All
July 2, 2026
Leanstral 1.5, a free Apache-2.0 licensed model with 119B total and only 6B active parameters, delivers a performance upgrade that makes formal verification more powerful and accessible than ever.
Leanstral 1.5 saturates miniF2F, solves 587/672 PutnamBench problems, and achieves a new state-of-the-art of 87% on FATE-H and 34% on FATE-X. Beyond benchmarks, it verifies complex code properties and uncovers previously unknown bugs in open-source repositories.
Training
Leanstral 1.5 goes through a three-stage process: mid-training, supervised fine-tuning, and reinforcement learning with CISPO. It leverages two RL environments:
- Multiturn environment: Given a theorem statement, the model must prove or disprove it, receiving Lean compiler feedback and refining across attempts.
- Code agent environment: Operates like a developer in a raw filesystem — edits files, runs bash commands, uses the Lean language server. Verified by a fork of SafeVerify.
Evaluation
- miniF2F: 100% on validation and test sets (saturated).
- PutnamBench: 587/672 problems solved; edges out Seed-Prover 1.5 high by 7 problems at ~300+ for Seed-Prover.
- FATE-H / FATE-X: New SOTA at 87 and 34 problems respectively.
- FLTEval: pass@1 from 21.9 to 28.9, pass@8 from 31.9 to 43.2, surpassing Opus 4.6’s 39.6 at one-seventh the cost.
Test-time scaling on PutnamBench is strongest seen from a formal-reasoning model: 44 problems at 50k tokens, 244 at 200k, 493 at 1M, 587 at 4M.
Code Verification Case Studies
AVL Trees: Proved O(log n) insertion/deletion time complexity over 2.7 million tokens and 22 compactions.
Bug Discovery: Automated pipeline across 57 repositories flagged 47 violated properties, 11 genuine bugs, 5 previously unreported on GitHub. One bug: zigzag decoding sign function in datrs/varinteger overflowed on Std.U64.MAX.
Availability
Apache-2.0 license. Weights on Hugging Face. Free API endpoint leanstral-1-5. Usable via Mistral Vibe with /leanstral agent.