AIが数学を形式化する時代、急ぐと「取り返しのつかない損害」をもたらす
How to Formalize All of Mathematics
OpenAIのリリース以降、AIは定理証明で目覚ましい成果を上げている。しかし、数学者たちは「すべてを急いで形式化する」動きに警鐘を鳴らす。質の低い形式化は資源の浪費にとどまらず、数学そのものに永続的な損害を与えかねない。Math, Inc.が試みた球充填定理の形式化では、AI生成コードの修正に手間がかかり、結局は破棄してやり直すことになった。本稿では、形式化を「うまくやる」ための具体的な懸念と、AIと共存する建設的なビジョンを示す。
うまくやれば、大規模で協調的な形式化の取り組みは数学的探求と発見を飛躍的に拡大できる。だが、やり方を誤れば、せいぜい資源の無駄で済むが、より可能性が高いのは、取り返しのつかない損害を与えることだ。