7月10日、New Scientistが「Mathematicians put AI to work on Fermat's last theorem」と題した記事を公開した。この記事では、数学者たちがフェルマーの最終定理の形式化プロジェクトにAIを投入し、予想を超える速度で進展が起きていること、そして人間の数学者の役割が問われ始めていることについて詳しく紹介されている。

たった1日で2万行のコードが倍増

ロンドン市内のホテルの一室に、25人の数学者・コンピュータサイエンティスト・AI研究者が集まり、1週間かけて取り組むワークショップが開催された。テーマは「フェルマーの最終定理の形式化」——その作業にAIを本格投入するというものだ。

フェルマーの最終定理とは、「aⁿ + bⁿ = cⁿ を満たす整数 a, b, c は、n が 2 より大きい整数のとき存在しない」という命題だ。17世紀に提唱されてから約350年間証明されず、1993年にアンドリュー・ワイルズがようやく証明したことで知られる。

インペリアル・カレッジ・ロンドンのKevin Buzzardは現在、ワイルズの証明（約100ページ）をプログラミング言語 Lean のコードとして形式化する5年間のプロジェクトを進めている。Leanは定理証明支援系（theorem prover）としても広く使われる言語で、数学的証明をコンピュータが検証可能な形式に変換する「形式化」の分野で標準的なツールとなっている。形式化されたコードは Mathlib と呼ばれる中央リポジトリに格納されており、現在200万行超の形式化済み数学が蓄積されている。

ワークショップ開始前の時点でプロジェクトのコードは計2万行だった。それが初日だけで倍の4万行になった。AIがサブ問題を次々と処理していった結果だ。

AIの急成長がプロジェクトの設計を変えた

Buzzardは当初、ワイルズの証明の最終論文部分だけを形式化し、それが依拠する1960〜80年代の約2000ページ分の数学は「正しいと仮定する」という方針でいた。ピラミッドの90%地点から頂上に向けて登るイメージだ。

その計画を変えたのは、AIの急成長だ。昨年12月ごろからAIの数学処理能力が急激に向上し、今年5月には80年未解決だったポール・エルデシュの問題がAIによって解かれた。

「静かに成功を確信していた。でも今は——やろうとしていたことが馬鹿げて見えてくる。それの10倍のことをやれるんじゃないかと感じている」（Buzzard）

現在は、ピラミッド全体を下から形式化する「完全版」を視野に入れている。5年間のプロジェクト期間中に当初の目標を達成するのはほぼ確実と見ており、そこからどこまで進めるかをAIの進化と費用次第で判断していく構えだ。

「スロップ」の上に次の層を積めるか

ワークショップでは、無料のオープンソースツールから米国スタートアップの最新モデルまで多様なAIが使われた。費用についてはイベント参加者も正確に把握していないが、1日あたり数千ポンドは軽く超えるという見方で一致しているという。

参加者のHang Lu Suは6ヶ月前にChatGPTを使ってLeanを独学し、今回のワークショップに参加している。彼女がファーストデイに体験したのは、同じ定理に対して自分が800行のコードを生成し、同僚が400行で解いたという出来事だ（原文では "lines" と表記されており、「語数」ではなくコードの行数と解釈するのが自然だろう）。どちらも証明としては成立するが、短い方が次のAI処理にも人間の読解にも有利だ。

AIが生成するコードの質的問題も浮上している。Buzzardによれば、AIのコードは冗長で動作が遅く、Leanの仕様変更でコンパイルが壊れるような実装を取ることもある。Mathlibのキュレーターたちは、たとえ定理を証明できていても、こうしたAI生成コードを大量に取り込むことには慎重だ。Mathlibに蓄積された既存コードは人間の数学者が丁寧に書いたものであり、効率・簡潔さ・可読性が担保されている。

Buzzardはこの状況を率直に表現している。

「その上に『スロップ（slop）』の層を積み上げている——スロップと呼ぼう——問題はその上に次の層を積めるか、それとも行き詰まるかだ」

「機械が証明して、人間に何が残るか」

技術的な課題の先に、より根本的な問いが浮かぶ。AIが定理を証明できるとして、それを人間が理解できなければ何を達成したことになるのか。

「我々は数学を愛し、重要だと思ってやっている。でもAIが登場して、なぜやっているのか、何の意味があるのかという問いが突きつけられる。機械が定理を証明しても人間が理解できなければ、何を成し遂げたのか？」（Buzzard）

38次元の球体や即座の応用が見えない抽象的な世界では、「人間が理解し鑑賞することで初めて数学の世界が存在する」という感覚があるとBuzzardは言う。AIの発展はその前提そのものを揺るがしている。

詳細はMathematicians put AI to work on Fermat's last theoremを参照していただきたい。