This page may contain stale information. Last updated: 2026-07-04
Overview
Leanstral is mistral AI’s open-weight model family for Lean 4 formal proof engineering — automated theorem proving, autoformalization, and code verification. Apache 2.0 licensed weights on Hugging Face plus free Labs API endpoint.
Leanstral 1.5 (July 2026)
- Architecture: 119B total / 6B active MoE; 256k context
Contradiction: Active parameter count — Mistral primary blog reports 6B active params; TestingCatalog secondary source cites 6.5B. Use Mistral-reported 6B unless independently verified. See 2026-07-02-mistral-leanstral-1-5-theorem-proving vs 2026-07-02-mistral-leanstral-testingcatalog.
- Benchmarks (Mistral-reported): 100% miniF2F saturation; 587/672 PutnamBench; 87% FATE-H; 34% FATE-X; FLTEval pass@8 31.9→43.2
- Practical: Found 5 previously unknown bugs across 57 OSS repos (e.g., varinteger overflow)
- Training: Mid-training, SFT, RL with CISPO
- Replaces Leanstral 2603 (retired June 30, 2026); Labs endpoint scheduled retirement Sept 30, 2026
Only closed-source Aleph Prover beats Leanstral 1.5 on PutnamBench per third-party reporting.