Mistral AIは2026年3月16日(現地時間)、形式証明アシスタント「Lean 4」向けに設計されたオープンソースコードエージェント「Leanstral」を発表した。このエージェントは、複雑な数学的オブジェクトやソフトウェア仕様の形式証明を支援する。Apache 2.0ライセンスの下でウェイトが公開され、Mistral vibeのエージェントモードと無料APIエンドポイントを通じて利用可能となる。
Mistral AIは、形式証明エンジニアリングタスクに最適化されたコードエージェント「Leanstral」の技術的詳細を明らかにした。本エージェントは疎なアーキテクチャを採用し、6Bのアクティブパラメータを持つと説明されている。Leanを完全な検証者として利用した並列推論により、既存のクローズドソース競合製品と比較して高いパフォーマンスと費用対効果を実現する。
同社は、Leanstralのトレーニングアプローチを詳細に記した技術レポートと、新たな評価スイート「FLTEval」も公開予定である。この評価スイートでは、FLT（フェルマーの最終定理）プロジェクトにおける形式証明の完了と新しい数学概念の定義に焦点を当ててベンチマークが実施される。
主要な既存コードエージェント（Claude Opus 4.6、Sonnet 4.6、Haiku 4.5）およびオープンソースモデル（Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B）との比較評価では、Leanstral-120B-A6Bが効率性において優位性を示した。特に、大規模なオープンソースモデルと比較して、少ないパスで同等以上のスコアを達成している。Qwen3.5 397B-A17Bのスコアは25.4であった。
コスト面では、LeanstralはClaudeスイートに対して高い費用対効果を提供する。例えば、pass@2でのスコアはSonnetを2.6ポイント上回りながら、Sonnetが549ドルのコストを要するのに対し、Leanstralは36ドルと大幅に低いコストで実行可能である。Claude Opus 4.6は品質でリードするものの、Leanstralの92倍のコストがかかるとされている。
ケーススタディとして、Lean 4の最新バージョンでの変更に関するProof Assistants Stack Exchangeの質問にLeanstralが回答し、コンパイルエラーの原因を診断して適切な修正を提案した事例が挙げられている。また、Rocqで記述されたプログラム定義をLeanに変換し、そのプログラムに関するプロパティを証明する能力も示された。
Leanstralは、Mistral vibeに直接統合されており、「/leanstall」コマンドやvibe —agent leanコマンドで利用できる。また、無料APIエンドポイントからもアクセスが可能である。
参考: mistral.ai — 2026年5月27日 09:00 (JST)