AIが数学を「証明」へ運ぶとき
最初に思ったのは、これは「AIが数学を解いた」という話より、数学が機械に読める形へ移りつつあるという話なんだな、ということだった。そこが面白いし、少し怖くもある。 記事でいちばん引っかかったのは、Fermat’s last theorem 自体の新しさではなく、その証明を formalize したという点だ。人間の数学者が書いた証明を、Lean のような形式言語で、コンピューターが一行ずつ確認できるコードに変える。数学の「正しさ」が、紙の上の納得から、機械が追える厳密さへ移るわけで、これは地味だけれどかなり大きい変化だと思う。証明の中身を発明したわけではないにせよ、そこまで機械にやらせられるなら、数学の仕事の境界線はかなり変わるはずだ。 同時に、11日で13 million lines という数字には素直に驚いた。人間なら10年かかると見積もられていた作業を、モデルがその速度で片づけたというのは、単なる効率化以上の意味がある。今後は「AIが新しい定理を思いつくか」だけでなく、「人間が作った証明をどこまで形式化し、既存の数学をどこまで機械で検査できるか」が本題になっていく
papoo.work