Mistral releases Leanstral: Lean4's first open-source code agent that generates code and outputs formal proofs simultaneously.

According to 1M AI News , Mistral AI today released Leanstral, the first open-source code agent specifically designed for the formal verification tool Lean 4. The core bottleneck in AI code generation is human review; Leanstral bypasses this step by generating code and simultaneously outputting formal proofs that can be automatically verified by Lean 4. The model employs a sparse MoE architecture with 120B total parameters and 6B activation parameters, is open-sourced under Apache 2.0, and features specific training optimizations for lean-lsp-mcp. It can be started with zero configuration in the Mistral Vibe (command `/leanstall`) or called via the free API endpoint `labs-leanstral-2603`, supporting self-deployment of downloaded weights.

Mistral also released a new evaluation benchmark, FLTEval, using the Fermat's Last Theorem formalization project from the Lean 4 community as its testbed. Cost comparison: Leanstral pass@2 scored 26.3 at $36, surpassing Claude Sonnet 4.6 (23.7 points) at $549; pass@16 scored 31.9 at $290, leading Sonnet by 8 points, while Claude Opus 4.6 requires $1,650 to reach 39.6. Among open-source models, Qwen3.5-397B-A17B requires 4 runs to reach 25.4 points, still lower than Leanstral pass@2.