Leanstral：Mistralが公開したLean 4形式検証用オープンソースコードエージェント

MistralがLeanstralをリリースした。数学的およびソフトウェアの形式検証に使用される証明支援系Lean 4専用に設計された初のオープンソースコードエージェントである。Apache 2.0でリリースされ、6Bアクティブパラメータのスパースアーキテクチャを採用。競合モデルよりも大幅に小型でありながら、FLTEvalベンチマークでClaude Sonnetを上回る（pass@2で26.3 vs 23.7）。しかもコストはわずか36ドル（対549ドル）。

Leanstralはlean-lsp-mcp経由のModel Context Protocol（MCP）拡張をサポートし、検証ワークフローにおいてAIエージェントから直接操作可能。3つのチャネルで利用可能：Mistral Vibeの/leanstralコマンドによるゼロセットアップ統合、無料APIエンドポイント（labs-leanstral-2603）、ダウンロード用のセルフホスト重み。

リリースには新しい評価スイートFLTEvalも含まれ、孤立した数学問題を超えて現実的な形式リポジトリタスクに取り組む。これにより、Leanstralはエージェント型AIと形式検証の新興交差点における重要なツールとして位置づけられる。エージェントが単にコードを書くだけでなく、その正しさを証明する領域である。

公式発表: https://mistral.ai/news/leanstral