Mistral AIは2026年6月30日、AIモデル「Leanstral 1.5」を公開しました。
数学の証明や、プログラムが正しいかを機械的に確かめる作業を支援するモデルです。
Leanstral 1.5は、形式証明ツール「Lean 4」向けに最適化されています。
自動定理証明と自動形式化を支援します。人が書いた内容をどこまで自動で処理できるのかは、資料に説明がありません。
Mistral AIは、Leanstral 1.5をLabs枠で無料利用できると案内しています。
具体的な利用方法や利用条件、性能の詳しい情報は、今回の資料だけでは分かりません。
出典名：GIGAZINE「Mistralが自動定理証明向けAI『Leanstral 1.5』リリース、Lean 4の証明作業を支援」
出典URL：https://gigazine.net/news/20260701-mistral-leanstral-1-5/