Leanstral
2026-03-16 · Publisher : Mistral AI · Domain : Artificial Intelligence
Mistral AI releases Leanstral, an open source Apache 2.0 agent of about 120 billion parameters (6 billion active) for formal proof engineering in Lean 4 and verifiable coding.
What changes
- Model designed for realistic Lean repositories rather than for competition mathematics alone.
- Integrated into Mistral Vibe (/leanstral command).
- Free or nearly free API endpoint for a limited period.
- Sparse architecture: about 6B active parameters.
### Specifications - Parameters: about 120B total (119B on the Hugging Face side), 6B active. - API identifier: labs-leanstral-2603. - License: Apache 2.0, downloadable weights. - Availability: API, Mistral Vibe, Hugging Face (Leanstral-2603). - Context, maximum output, knowledge cutoff: not disclosed. ### Pricing | Item | Price | |---|---| | API endpoint | Free or nearly free for a limited period | | FLTEval evaluation cost, pass@2 | 36 USD | | FLTEval evaluation cost, pass@16 | 290 USD | The pass@k amounts are benchmark evaluation costs, not per-token prices. ### Benchmarks | Measure (FLTEval) | Score | |---|---| | pass@2 | 26.3 (Claude Sonnet: 23.7, for 549 USD) | | pass@16 | 31.9 | Scores published by the vendor. ### Key takeaways An open, low-cost formal verifier is of interest to teams that want guarantees on critical code, beyond a simple review by an LLM.
Links
Tags : LLM, Mistral, Leanstral, Open Source, Preuve formelle, Code