仏Mistral AIは、複雑な数学的定理の証明やプログラムの形式的検証（Formal Verification）に特化した専門オープンAIモデル「Leanstral 1.5」を公開しました。
本モデルは、数学の定理証明記述言語である「Lean」を用いた形式的ロジック検証に最適化されており、ソフトウェアのバグ排除や数学的証明のコード化において極めて高い精度を誇ります。開発者はミッションクリティカルなシステムや高信頼性が求められるスマートコントラクトの正確性を自動検証させることが可能となります。
最先端の数理解析能力を持つオープンモデルの登場により、ソフトウェア検証やアカデミックな研究現場におけるAI活用の可能性が大きく拡がると期待されています（一次ソース：Mistral AI公式発表）。