(>>918の続き)
3. 最新の「AI×数学」の動向
最近では、生成AIの「発想力」と、形式検証ツールの「厳密さ」を
組み合わせたハイブリッド型の研究が進んでいます。
・AlphaProof / AlphaGeometry: Google DeepMindが開発。
 数学オリンピック級の難問を解き、
 その解答を形式検証システムで自己チェックすることで、
 100%正しい証明を生成することに成功しています。
・Leanとの連携: 人間が書いた「ふんわりとした数学の文章」を、
 AIが「厳密なコード(Lean)」に翻訳し、
 コンピュータに正否を判定させる試みが加速しています。
 arXiv
 arXiv+4