Mistral Releases Leanstral
3 hours ago
- #Lean 4
- #formal verification
- #AI coding agents
- Leanstral is the first open-source code agent designed for Lean 4, aimed at formal verification of implementations.
- It is highly efficient with 6B active parameters and optimized for proof engineering tasks.
- Leanstral is released under Apache 2.0 license, available in agent mode within Mistral vibe and through a free API endpoint.
- The model supports arbitrary MCPs through vibe and was trained for maximal performance with lean-lsp-mcp.
- Benchmarks show Leanstral outperforms larger open-source models and offers competitive performance at a fraction of the cost compared to Claude models.
- Case studies demonstrate Leanstral's ability to diagnose and fix issues in Lean code and translate programs from other languages to Lean.
- Leanstral is available for immediate use via Mistral Vibe, a free API endpoint, or by downloading the model weights.