#形式化

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

Anthropic が公開したのは、Fermat の最終定理について「新しい数学の発見」ではなく、「既にある証明を Lean で最後まで機械検証できる形に落とし込んだ」成果だ。しかもその作業は、人間が細かく手を動かして積み上げたというより、Claude が 11 日間かなり自律的に進めたものだという。数学の世界では、証明が正しいかどうかを読む人間が何週間も何か月もかけて確かめることがある。そこに AI と proof assistant の組み合わせがどこまで食い込めるのか、Anthropic はかなり強い実演を見せた格好だと思う。 Anthropic の発表によると、Claude は Fermat の最終定理の proof を Lean という programming language に書き直し、computer-checked な形で最後まで通した。Fermat の最終定理とは、正の整数 a, b, c について aⁿ + bⁿ = cⁿ を満たす解は n > 2 では存在しない、という有名な命題だ。17世紀に Pierre de Fermat が書き残したもので、長く未解決だっ