Leanstralとは
Leanstralとは、Mistral AIが2026年3月に公開した、Lean 4で形式証明を進めるためのオープンソースのコードエージェントです。普通のコード生成AIが「それらしい実装案」を出すのに対し、Leanstralは証明器で確かめられるコードや定理の作業に寄せて設計されています。
英語表記：Leanstral
普通のコード生成AIとの違い
Lean 4は、数学の定理やソフトウェア仕様を機械的に確かめるための証明支援システムです。Leanstralは、そのLean 4の環境で証明を書いたり、未完成の証明を埋めたりする作業を想定しています。言い換えると、文章のうまさよりも、検証可能な形で正しさへ近づけることが中心です。
Mistralが発表で挙げた課題は、AIが書いたコードを人が確かめるための時間と専門知識でした。最先端の数学研究から止まってはいけない基幹ソフトウェアまで、間違いの許されない領域ほど人のレビューが開発の速さを縛るという見立てです。そこでAIに実装させるだけでなく、厳密な仕様に照らして正しさまで証明させる。人はAIの書いたロジックを直す役から、何を満たすべきかを伝える役へ回る、という将来像を描いています。
Leanstralは、今も使えるのか
Mistralのモデル一覧では、Leanstral（版26.03）のAPIは2026年5月22日に非推奨、6月30日に提供終了とされ、移行先には同じ6月30日に公開されたLeanstral 1.5が示されています。一方で、重みはApache 2.0ライセンスのままHugging Faceで公開されています（2026年9月時点）。APIの提供終了と、モデル本体を入手できるかどうかは別の話です。
見落としやすいのは移行先のほうです。Leanstral 1.5の公開を伝えるMistralの変更履歴には、そのLeanstral 1.5も2026年9月30日に提供を終えると書かれています。APIで使い続ける計画なら、組み込む前にその時点の移行先をモデル一覧で確かめておくのが安全でしょう。
Topic腕試しの題材は、数学コンテストではなく「フェルマーの最終定理」
MistralはLeanstralの評価に、単発の数学問題ではなく、フェルマーの最終定理のリポジトリに実際に出された変更（プルリクエスト）を使いました。変更ごとに、証明をすべて書き上げ、新しい数学の概念を正しく定義できるかを確かめます。この評価はFLTEvalと名付けられ、コンテスト数学に寄りがちだった物差しを、現実の証明作業での使いやすさへ移す狙いだと説明されています。
Leanstralに関するよくある質問
- Leanstralは普通のプログラミングAIと何が違いますか？
- 一般的なコード補完より、証明として通る形にすることへ寄っています。人のレビューだけに頼らず、機械で検証できる作業へ寄せる点が特徴です。
- Lean 4を知らない人はLeanstralをどう理解すればよいですか？
- Lean 4は、答えが正しいかを機械的に確かめるための環境です。Leanstralは、その環境でAIが証明や検証作業を手伝うものだと捉えると分かりやすいでしょう。
- Leanstralはどれくらいの規模のモデルですか？
- モデルカードの表示では全体で1,190億パラメータ、1トークンごとに働くのは65億です。Mistralは、処理を軽くするために全体のごく一部だけを使う疎な構造にしたと説明しています。
