Mistral が Leanstral-1.5-119B-A6B をリリース ── 数学の証明すらこなす最強のコードエージェント
数学の定理証明や複雑なコードの仕様検証をAIに任せられたら？ Mistralが「Leanstral-1.5-119B-A6B」をHugging Faceにリリースした。Lean 4という証明支援システムのために特化して作られたオープンソースのコードエージェントモデルで、そのスペックと設計思想にかなりの本気度を感じる。
▸何が変わったのか
Mistral Small 4ファミリーの一員として登場。テキストと画像を入力できるマルチモーダル対応だ。
アーキテクチャはMoE（Mixture of Experts）。128のエキスパートのうち、トークンごとに4つをアクティブ化する仕組み。全体で119Bのパラメータを持ちつつ、実際に動くのは6.5Bという効率重視のバランス。
最大コンテキスト長は256kトークン（推奨は200k以下）。
単発の回答だけでなく、Mistral VibeというCLIツールからエージェントとして動かせる。VS Codeのターミナルで立ち上げて、定理の証明やコード修正を直接お願い可能。`–yolo`オプションをつければ、モデルの変更を自動承認して数時間かかるような長期間タスクも自律的に回してくれる。
◈前モデル / 競合との比較
以前リリースされたLeanstralモデルのアップデート版にあたる。既存のクローズドソースの代替モデルと比較して、高いパフォーマンスとコスト効率の両立を強くアピールしている点が最大のポイント。
◈技術背景と意義
そもそもLean 4とは、簡単に言えば「数学の複雑な証明やプログラムの厳密な仕様を、コンピュータが理解できる形で書いて検証する」ための言語。高度な数学の対象から、Rustコードの安全性の確認までを扱える。
こうした厳密な論理の世界は、これまで人間の専門家が膨大な時間をかけて取り組む領域だった。それをAIエージェントが自律的に補助し、検証作業をこなしてくれるのは本当にエポックメイキングな出来事だ。
▸こんな人・用途に
・複雑な数学の定理証明をAIと一緒に進めたい研究者や学生
・Rustコードの仕様チェックやプロジェクト内のバグ修正を自動化したいエンジニア
・数時間規模の長期間タスクを自律的に回してほしい開発者
◆入手方法・リンク
Hugging Faceでオープンソースとして公開中。利用するにはMistralのアカウント設定で「Enable Labs models」をオンにし、APIキーを取得。専用CLIツールのMistral Vibeをインストールし、`/leanstall` コマンドを打ち込めば環境構築が完了する。ローカルのvLLMサーバー環境で動かすことも可能だ。
SOURCE: Mistral (2026-07-01)
