数学は「音楽院」入りするのか？AIが証明した定理が問いかけるもの

Is mathematics about to enter the conservatory?

ClaudeがLeanでフェルマーの最終定理の証明を形式化した同じ週に、AI支援によって「球面ハドヴィガー予想」が証明されたとする論文が発表された。この予想は1974年から未解決だったもので、著者らはOpenAI Codexを証明の詳細の開発やギャップの発見に使用したと述べている。数学者の仕事はAIによる影響を最も受けるとされていたが、その時がついに来たのかもしれない。本稿では、純粋数学がすでに「アカデミー」という名の音楽院にあると指摘し、AI時代における数学者支援のあり方を問う。