Mistral、Lean 4向けオープンソースコードエージェントLeanstralを公開

Mistralは2026年3月16日、Leanstralを公開し、これをLean 4向けに設計された初のオープンソースcode agentだと位置づけた。Lean 4はformal verificationやtheorem provingで使われるproof assistantであり、今回の発表は一般用途モデルを流用するのではなく、formal workflowに最適化した専用agentが必要だという考え方を前面に出している。

同社の説明では、Leanstralの価値は単純な規模競争ではなく、効率と実運用への適合性にある。Mistralはこのモデルが6B active parametersで動作し、単発の数学問題ではなく実際のformal repositoryで作業するよう訓練されたと説明した。さらに、competition math偏重の評価から離れるため、新しい評価セットであるFLTEvalと技術レポートも公開予定だとしている。

• Lean 4 workflow向けに特化
• Apache 2.0ライセンスで公開
• Mistral Vibeに統合され、labs-leanstral-2603 APIでも利用可能
• weightsをダウンロードしてself-hostingも可能

ブログでは、LeanstralがFLTEvalでより大きなopen-source modelに対して効率面で優位だと主張している。公開比較では、少ないpassで競争力のあるスコアに到達し、追加passを許可するとさらに性能が伸びる構図が示された。formal methodsの現場では、絶対性能だけでなく、latency、compute cost、構造化されたrepository内での安定動作が重要なため、この訴求は実務的だ。

今回の発表が示すのは、formal verificationが研究用途だけでなく開発ツールの一部として扱われ始めていることだ。open license、製品統合、実運用寄りのbenchmarkを同時に出すことで、Mistralはverified codeとproof-oriented programmingを実用カテゴリとして押し上げようとしている。安全性重視のsoftwareやtheorem provingの現場にとって、Leanstralは注目度の高い新しい選択肢になりそうだ。