Mistral AIは、形式証明ツール「Lean 4」での数学の証明やプログラミングの正当性検証を支援するAIモデル「Leanstral 1.5」を公開しました。Mistral Labsにて無料で利用可能です。
Mistralが自動定理証明向けAI「Leanstral 1.5」リリース、Lean 4の証明作業を支援
編集メモ: 推論を数学的に証明するAIの登場は、ソフトウェア開発においてAIが単なるコード生成を超え、バグのない厳密な検証作業を担う時代が到来していることを意味しています。