最初に思ったのは、これは「AIが数学を解いた」という話より、数学が機械に読める形へ移りつつあるという話なんだな、ということだった。そこが面白いし、少し怖くもある。
記事でいちばん引っかかったのは、Fermat’s last theorem 自体の新しさではなく、その証明を formalize したという点だ。人間の数学者が書いた証明を、Lean のような形式言語で、コンピューターが一行ずつ確認できるコードに変える。数学の「正しさ」が、紙の上の納得から、機械が追える厳密さへ移るわけで、これは地味だけれどかなり大きい変化だと思う。証明の中身を発明したわけではないにせよ、そこまで機械にやらせられるなら、数学の仕事の境界線はかなり変わるはずだ。
同時に、11日で13 million lines という数字には素直に驚いた。人間なら10年かかると見積もられていた作業を、モデルがその速度で片づけたというのは、単なる効率化以上の意味がある。今後は「AIが新しい定理を思いつくか」だけでなく、「人間が作った証明をどこまで形式化し、既存の数学をどこまで機械で検査できるか」が本題になっていくのではないかと思う。もし本当に数学の大きな成果が次々と formalize されていくなら、見落としや誤りの発見も、かなり別のスケールで起きそうだ。
ただ、ここで言う「証明した」という言葉には少し注意が要る気もした。この記事の面白さは、AIが独力で Fermat を解いたというより、人間の数学を機械検証の世界に持ち込んだことにある。そこを混同すると、過大評価にも過小評価にもなる。けれど、その中間にある現実こそ重要で、たぶん数学はしばらくのあいだ、人間が考え、AIが整え、機械が監査する、そんな共同作業に寄っていくのだと思う。
参考: Anthropic AI ‘formalizes’ proof of Fermat’s last theorem — a milestone for mathematics
