今週ロンドンに研究者が集まり、高度なAIモデルを用いてフェルマーの最終定理の形式化を加速させている。このワークショップでは、アンドリュー・ワイルズが1993年に発表した証明を、コンピュータによる検証が可能なLeanコードへ変換することに焦点を当てている。進捗は急速で、初日だけでコード行数は倍増した。
数学者、コンピュータ科学者、AI専門家ら25名がロンドン中心部のホテルに集まり、インペリアル・カレッジ・ロンドンのケビン・バザード教授が主導するプロジェクトに取り組んだ。2024年に資金提供を受けたこの5カ年計画は、同定理を形式化数学のリポジトリである「Mathlib」に追加することを目指している。
ワークショップ開催前、このプロジェクトのコード行数は2万行だったが、初日終了時には4万行に達した。バザード教授は、昨年12月以降のAI性能の飛躍的な向上により、当初の計画よりも多くの基礎的な数学的概念を扱うことが可能になったと述べた。
同じくインペリアル・カレッジ・ロンドンのハン・ルー・スーは、このプロセスを知的作業の工業化であると評した。参加者はClaudeを含むAIモデルを用いてコードの生成や修正を行っているが、AIが生成したコードの冗長性や長期的な保守性については懸念も残っている。
バザード教授は、プロジェクト終了までに当初の目標が達成されるとの確信を示した。チームが定理を支える「ピラミッド」構造のどの程度まで進展させられるかは、今後のAI技術の発展次第となる。