人間の数学者は反例によって凌駕されている

← Formalizing Fermat workshop 人間の数学者は反例によって凌駕されている 2026年7月20日投稿 by xenaproject 反例にとって、この数週間は興味深いものでした。この記事は、形式化、AIツール、そして特に反例の世界で何が起こっているかについての私の視点を基本的に述べています。 単位距離 2ヶ月前の今日（2026年5月20日）、ChatGPTは離散幾何学におけるErdősの単位距離予想を反証しました。これは今では古いニュースですが、どこかで始めなければなりませんでした。発表には、人間の数学者からの証言が伴いました。その多くは私が知っており、信頼していた人々でしたが、彼らは（早期アクセスを与えられ、それをチェックした）議論を信じていると述べました。証明の基本的な構造は、1960年代のGolodとShafarevichによる数論の深遠な定理が、予想に対する反例を構築するために使用できるということでした。 私が中間的な危機を迎え、技術的な詳細に関して多くの人間の数学者を信頼しなくなったことを認識し、Leanを発見し、対話型定理証明器が数学の将来において重要な役割を果たすべきだと主張し始めてから、もう9年になります。ですから、もちろん私の最初の質問は「反例はLeanで形式化されているか？」でした。答えは「いいえ」でした。しかし、1週間も経たないうちに（2026年5月26日）、私はFields Medal受賞者のMike Freedmanからメールを受け取りました。Mikeは現在、チューリング賞受賞者で「AIのゴッドファーザー」であるYan LeCunが共同設立した企業、Logical Intelligenceの最高科学責任者です。Mikeは、彼らのシステムがChatGPTが生成した論文全体をLeanで自動形式化したと私に伝え、私がそれを確認できるか尋ねました。私は確認し、私のポスドクであるThomas Browningも確認しました。そして、まさにLogical Intelligenceが行ったことはこれでした。彼らは、深遠な数論の定理がErdősの反例を意味するという主張を正確に形式化していました。画期的なLLM生成数学がリアルタイムで形式化されています。興味深いデータポイントです。 もちろん、ここには象徴的な問題があります。それは、証明に100ページ以上かかる深遠な数論の定理です（それは大域的な類体論の巨大な部分を必要とします。これは20世紀初頭に開発された理論であり、まだ短い証明が存在しません。圧縮が困難であることが証明されています）。2025年に、Richard Hillと共に類体論の形式化に関するClay Summer Schoolを運営しましたが、1年後には局所的なケースをほぼ完了しました（それは私の学生Edison Xieの現在の博士課程プロジェクトです）。大域的なケースは未解決のままであり、実際、2025年に大域的な類体論を形式化することはファンタジーのように思われました。 1ヶ月後、2026年6月26日、私の可能性の認識は再び変わりました。Boris AlexeevはLean Zulipで、彼がChatGPTをErdős反例の完全な形式化に導いたと発表しました。数学の公理以上のものは何も仮定していません。BorisはOpenAIで働いており、彼らの新しいモデルSolを使用して自動形式化を行いました。Borisはコードを公開し、AI生成（時にはひどい、時にはまともな）コードのどこかに、大域的な類体論の本当に難しい定理の証明があることに気づくのに時間はかかりませんでした。また、Solがプロジェクトに取り組んでいた3週間で120万行のLeanコードを生成したことも興味深かったです。Leanの素晴らしい（利益相反の宣言：私はメンテナーです）数学ライブラリmathlibはわずか230万行のコードで、作成に9年かかりました。おそらく、この時点で本当に理解できたのは、大規模なAI生成の数学的発展は避けられないということです。AI生成コードは信頼できないので、私はそれを自分のマシン上のサンドボックスで実行しました（Leanは結局のところプログラミング言語であり、悪意のあるLeanコードはコンピュータ上で任意のコマンドを実行できます）。実際、それは数体のコホモロジーに関する非自明な定理を証明していました。すごい。 オーダーnの群スキーム Borisの発表の1週間後、7月初旬、私はFormalizing Fermatワークショップの運営方法について熱心に考えていました。このワークショップはLogos Researchによって後援されました。Logosは、Logical Intelligence（およびHarmonic、Axiom AI、Moonshot AIなど）と同様に、数学を自動形式化するツール（人間言語からLeanへの翻訳）を持っており、mathlibを基盤としています。Logosは、ワークショップ中に一度に5人しかシステムを使用できないと私に伝えました。参加者は25人だったので、私はすべての参加者に、順番待ちの間に実験できるものがあるように、1ヶ月間Claude Maxサブスクリプションを私が購入すると伝えました。ワークショップは7月6日から10日までで、Claude Maxサブスクリプションは参加者にClaude Fableへのアクセスを提供しました。少なくとも火曜日7日まで、それ以降は停止される予定でした。OpenAIが私の活動を知ると、彼らもすべての参加者に1ヶ月間無料のChatGPT Proアクセスを提供しました。これは、ChatGPT Solが9日にリリースされる予定だったため、大きな取引でした。したがって、基本的にすべての参加者は、ワークショップの5日間のうち4日間、SolとFableにアクセスでき、Logosのツールは1週間すべて利用できました。実際、Fableへのアクセスは7日に削除されなかったので、私たちはさらに良い状況でした。 Logosのツールがどれほど優れているかは確信が持てませんでしたが、私は自身のフェルマー最終定理の証明のために、Leanでの有限平坦群スキームの理論の発展を必要としていました。そのため、私はその分野の古典的な論文をFableとChatGPTにアップロードし、それらをまとめて自然言語で理論の解説を記述させました。私はこのPDFドキュメントをワークショップの前日にLogosに渡しました。ワークショップ初日に、彼らはPDFの主張の1つが偽であり、明示的な反例を見つけたと述べました。別の反例です！私は確認し、確かにLLM生成のPDFは、標準的な構成を説明する際に単純に間違っていました。誤報でした。私もPDFを読んでいる間にこれを見落としていました。AIが再び反例を見つけたのは興味深いことです。私はPDFを修正しました。 AIは単に「この議論はよくわからない」と言うのではなく、「この議論が単純に間違っているという証明がここにあります」と言ったのは興味深いことです。これははるかに強力な声明です。有限平坦群スキームの理論の発展が軌道に戻ったので、私はFLTワークショップにリラックスして戻ることができました。 7月7日火曜日、私は昼食時にAkhil Mathewの向かいに座りました。AkhilはUChicagoの数学教授で、利用可能なツールを実験していた参加者でした。私たちはAIが取り組む可能性のある質問について話し合い、AkhilはGrothendieckの古い質問、すなわち「オーダーnのすべての有限自由群スキームはnによって殺されるか？」を提起しました。Deligneは可換ケースでこの結果を証明しており、Grothendieckは基底が還元された場合に証明しており、Rene Schoofはさらに多くのケースで証明しており、昨年Emiliano Tortiが発表した論文で、さらに一般的なケースで証明していました。私は、これがAIに考えさせる素晴らしいことだと述べました。 ワークショップが終了した翌日の土曜日、7月11日に、AkhilからDMを受け取り、Solが反例を見つけたと告げられました。彼は私に12ページのPDFを送ってきました。私はすぐに、AI生成の非形式的な数学を読むつもりはないと返信し、彼に全体をLeanで形式化してくれるように頼みました。4時間後、彼は再び返信し、Fableが全体を自動形式化したと述べました。 私は1076行のLeanファイルをスキャンし、コードが私のハードドライブ上のすべてのファイルを削除しないことを確認しました（Leanはプログラミング言語なので、これは可能です）。それが定理のみであると確信した後、私はラップトップでそれをコンパイルしました。合計で5分もかからずに、（a）主張された定理のステートメントがmathlibの概念のみを使用していること（したがって、HopfAlgebraのようなものは数学者がHopfAlgebraと考えるものを意味すると信頼できる）、（b）主張された定理のステートメントが反例が存在するというものであったこと、そして（c）証明がコンパイルされたことを確認できました。この時点で、私たちは…