Mistral Releases Leanstral: First Open Source Code Agent for Lean4, Generating Code and Formally Proving It

According to 1M AI News monitoring, Mistral AI today released Leanstral, the first open-source code agent designed specifically for the formal verification tool Lean 4. The core bottleneck of AI code generation is human review. Leanstral allows AI to generate code while simultaneously outputting a formal proof that can be automatically verified by Lean 4, bypassing this step. The model adopts a sparse MoE architecture with a total of 120B parameters and 6B activation parameters. It is open source under the Apache 2.0 license and has been specially trained and optimized for lean-lsp-mcp. It can be launched with zero configuration in Mistral Vibe (command `/leanstall`), or invoked through the free API endpoint `labs-leanstral-2603`, supporting weight downloads for self-deployment.

Mistral also simultaneously released a new evaluation benchmark FLTEval, using the Fermat's Last Theorem formalization project from the Lean 4 community as a testbed. Cost comparisons: Leanstral pass@2 scores 26.3 at $36, surpassing the $549-cost Claude Sonnet 4.6 (23.7 points); pass@16 scores 31.9 at $290, leading Sonnet by 8 points, while Claude Opus 4.6 requires $1,650 to achieve 39.6 points. In the open-source model, Qwen3.5-397B-A17B needs to run 4 times to reach 25.4 points, still below Leanstral pass@2.