AIがフェルマーの最終定理をLean史上最大の証明に変換

フェルマーの最終定理が初めてコンピューターで検証可能なコードに変換され、わずか11日間で1,300万行の形式的証明が作成された。AIエージェントの一群が、数学的論理の検証用に設計されたプログラミング言語Leanで作業を完了するために必要な、約2万9,500の中間定理を構築した。

この成果は、1990年代にアンドリュー・ワイルズとリチャード・テイラーが完成させた人間による証明を置き換えたり、拡張したりするものではない。確立されたその論証を、コンピューターが段階ごとに確認できる形式に変換したものだ。この定理は、nが2より大きい場合、aⁿ + bⁿ = cⁿを満たす正の整数は存在しないとする。

人間の専門家は時折、大局的な指針を与えた。エージェントは当初、連携に苦戦したが、完了した課題を把握し、次に取り組む課題を選ぶための協働ツールProve2Meを使うことで成功した。数学者のケビン・バザードは、完成したコードをコンパイルしてLeanの標準的な検証を実行し、必要な数学的内容が実際に構築されていると結論づけた。

この形式化の規模は、Leanの数学における主要な共有ライブラリMathlibの5倍を超える。その規模は、AIが近い将来、数学文献の大きな部分を検証可能なコードへ変換する作業を支援し得ることを示唆している。ただし、これほど膨大な出力を精査し、人間にも理解できるものにすることは、依然として大きな課題だ。