Leanstral
Leanstral, a 120B sparse model with 6B active, is Mistral's open agent for Lean 4 formal proofs, scoring 26.3 at pass@2 for $36.
An open agent for Lean 4 proof engineering, trained so humans need not review each proof. Mistral reports pass@2 score 26.3 for $36 versus Claude Sonnet 23.7 for $549. At pass@16 Claude Opus still scored higher (39.6 at $1,650 vs 31.9 at $290).
- Date
- Monday, 16 March 2026
- Lab
- Mistral AI
- Kind
- open-weights
- Access
- open weights
Figures
| Measure | Value | Measured by |
|---|---|---|
| Pass@2 score on Mistral's Lean proof eval | 26.3 at $36 vs Claude Sonnet 23.7 at $549; pass@16 31.9 at $290 vs Opus 39.6 at $1,650 | company |
Cost comparisons are Mistral's. Mistral also claims about 45x savings versus Opus, but Opus scored higher at pass@16.
Sources
This record was checked against its sources on 6 October 2026. How we check