Leanstral 1.5：すべての人のための証明の豊かさ
Mistral AIが「Leanstral 1.5」を発表。これは、Lean定理証明器とMistralの大規模言語モデルを組み合わせ、形式検証や数学的推論における証明の生成を促進するツール。証明の「豊かさ（abundance）」を民主化し、研究者や開発者がより簡単に厳密な証明を構築できるよう支援する。
背景メモ
Mistral AI（仏パリ拠点）が2025年5月に発表した「Leanstral 1.5」は、Lean形式の定理証明（形式的検証）を自動生成する大規模推論モデル。Leanは数学の証明を計算機でチェック可能な形式に落とし込む言語で、ソフトウェアのバグゼロ検証や数学論文の正しさの機械確認に使われる。従来は熟練者だけが書けたこれらの証明を、Leanstralは自然言語の数学問題やコードから自動生成する。同社はこれに先立ち、「Lean 4」の証明を生成するデータセット「Leanstral-1.5-Instruct-Data」を公開し、コミュニティが独自にモデルをファインチューンできるようにしている。背景として、OpenAIのo1など「推論（思考）モデル」の流行があり、数学・コード分野での応用が加速中。MistralはEuroHPCの超算力を使い、欧州発のオープン寄り戦略で競合（OpenAI・Google・Metaなど）に対抗している。