ここ数週間、反例に関する動きが活発です。この投稿は、主に形式化、AIツール、そして特に反例に関する世界の動きについての私の視点です。

単位距離

2ヶ月前（2026年5月20日）、ChatGPTが離散幾何学におけるErdősの単位距離予想を反証しました。これはすでに古いニュースですが、まずはここから始めなければなりません。発表には、私が知る人間の数学者たちの証言が添えられ、そのうち何人かは信頼できる人々で、彼らはこの主張を信じていると述べていました（彼らは事前にアクセスを許可され、内容を確認していました）。証明の基本的な構造は、1960年代にGolodとShafarevichが証明した数論の深い定理を用いて、予想に対する反例を構成するというものです。

私が中年の危機を迎え、多くの人間の数学者を技術的な詳細に関しては信用しなくなり、Leanを発見し、対話型定理証明器が数学の未来において重要な役割を果たすべきだと主張し始めてから9年が経ちました。当然、私の最初の質問は「この反例はLeanで形式化されているのか？」でした。答えは「いいえ」でした。

しかし、その1週間も経たないうち（2026年5月26日）、フィールズ賞受賞者のMike Freedmanからメールが届きました。Mikeは現在、チューリング賞受賞者で「AIのゴッドファーザー」と呼ばれるYan LeCunが共同設立したLogical IntelligenceのChief Science Officerを務めています。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 workshopの運営方法について深く考えていました。このワークショップはLogos Researchが後援しており、Logical Intelligence（およびHarmonic、Axiom AI、Moonshot AIなど）と同様に、mathlibに基づいて数学を自動形式化（人間の言語からLeanへの翻訳）できるツールを持っています。Logosはワークショップ中に一度に5人しかシステムを使えないと言い、参加者は25人いたので、私は参加者全員に1ヶ月間Claude Maxサブスクリプションを購入すると伝え、Logosのツールが使えない時に実験できるようにしました。ワークショップは7月6日から10日で、Claude Maxサブスクリプションにより参加者は少なくとも7日火曜日までClaude Fableにアクセスできました。OpenAIが私の計画を知ると、参加者全員に1ヶ月間無料のChatGPT Proアクセスも提供してくれました。これは大きな意味がありました。なぜならChatGPT Solが9日にリリースされる予定だったからです。つまり、基本的にすべての参加者がワークショップの5日間のうち4日間SolとFableにアクセスでき、Logosのツールには1週間を通じてアクセスできることになりました。実際、Fableへのアクセスは7日に削除されなかったので、私たちはさらに良い状況でした。

Logosのツールがどれほど優れているかはわかりませんでしたが、進行中のFermatの最終定理の証明のためにLeanで有限平坦群スキームの理論を発展させたいと考え、FableとChatGPTにこの分野の古典的な論文をいくつかアップロードし、自然言語で理論の解説を書くようにしました。私はワークショップの前日にこのPDF文書をLogosに渡し、ワークショップ初日に彼らはPDF内の主張の1つが誤りであり、明示的な反例を見つけたと言いました。また別の反例です！私は確認しましたが、LLM生成のPDFは標準的な構成を説明する際に単に間違っていただけでした。誤報でした。私自身もPDFを読んでいて見逃していました。AIが再び反例を見つけたのは興味深いことです。私はPDFを修正しました。AIが単に「この議論がよくわかりません」と言うのではなく、「この議論が単に間違っているという証明はここにあります」と述べたのは興味深いことであり、はるかに強力な主張です。

有限平坦群スキームの理論の発展が軌道に戻ったので、私はFLTワークショップにリラックスして参加できました。7月7日火曜日、私は昼食時にAkhil Mathewの向かいに座っていました。AkhilはUChicagoの数学教授で、利用可能なツールで実験していた参加者の1人でした。私たちは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のようなものは数学者がホップ代数について考えるものとして信頼できる）、(b) 主張された定理の主張が反例の存在であること、(c) 証明がコンパイルされることを確認しました。この時点で、私たちは反例を得たことを知っていました。位数4の群スキームで、4で殺されないものです。私はAkhilに、この反例でmathlibにPRを作成するよう提案しました。彼はそうしました。私はまた、彼に「機械がGrothendieckの60年前の代数幾何学の問題を解決した」というプレスリリースを作成するよう提案したかもしれませんが、この時点で私はほとんどこれらのすべてに免疫ができていました。メディアが「機械がErdősによる問題を解決した」と「機械がGrothendieckによる問題を解決した」を区別できるかどうかは明らかではありませんでした。個人的には後者の方がはるかに興味深いと感じていました。もちろん、Grothendieckの反例はErdősの反例よりもはるかに簡単でした（100万行ではなく1000行）。私が言いたいのは、私が個人的に興味を持つ数学の分野だということです。私はAkhilに、機械は反例を見つけるのが非常に上手くなっているようだと指摘し、次はHodge予想を試してみるよう提案しました。

モジュラリティ持ち上げ定理

この時点で一歩引いて、人間の専門家がこの種の事柄に対してどのような態度を持っているかを調査する価値があると思います。7月14日火曜日、私はImperialで働き、Grothendieckの反例が昼食時の話題でした。教員の一人（名前は伏せます）が私に、反例が非常に簡単に見つかったという事実は、人間がこの問題について十分に考えていなかったことを示していると述べ、Grothendieckの60年前の問題は実際には取り組む価値がないことを示唆しました。私は彼に、私のキャリアの早い段階でこの問題に1週間真剣に取り組んだことがあったとは言いませんでした。私の同僚は今、悲嘆の5段階を経験していると思います。現在、彼らは否定の段階にあるようです。

昼食後、私は私の博士課程学生Andrew Yangと会いました。彼はLeanでモジュラリティ持ち上げ定理を形式化する作業をしていました。これは私のFLT作業に不可欠なものです。AndrewはLogos FLTワークショップに参加し、現在SolとFableの両方にアクセスできました。彼は、これらのツールを使って25万行のLeanコードを書き、基本的に2週間の期間でプロジェクトを完全に完了したと述べました。

数日前、私はImperialの数学部の教授からメールを受け取り、私たちの大学院生の一部がSolやFableのようなモデルにアクセスするために月額200ドルを支払っていることに驚いていると述べていました。彼は、これらの人々は気が狂っていると思っていると言いました。私はすぐに返信しませんでした。しかし、Andrewと会った後、私は教授に返信し、私の意見では、これらのツールにアクセスするために月額200ドルを支払わない博士課程学生は気が狂っていると伝えました。実際、ワークショップ中にハーバードの博士課程学生Bryan Wangから、ハーバードはすでにハーバードのすべての博士課程学生、ポスドク、教員に無料のFableアクセスを提供していることを学びました。

Jacobian予想

しかし、Akhilに戻りましょう。彼が私のHodge予想を反証するというアイデアを真剣に受け止めたかどうかはわかりません。しかし、彼はこれらの extraordinary な新しいAIツールがあれば、反例が今すぐ低空飛行の果実かもしれないと深く理解したようです。彼はLevent Alpögeと代数幾何学でより多くの反例を見つけるアイデアについて議論し、12時間前、LeventはXに投稿し、FableがJacobian予想に対する反例を見つけたと述べました。これは大きな意味があります。これは代数幾何学における有名な問題で、100年間未解決であり、多くの人々が考えていました。それは2026年のワールドカップ決勝中に解決されたようです。

私は今日起きたらAkhilから「もう1つのPRを作成しましょうか？」というDMを受け取りましたが、彼は遅すぎました。Paul Lezeauがすでに手動で反例を形式化し、DeepMindのFormal Conjectures repoにPRを作成していたからです。Mathlibには数学の大きな予想リストは含まれていませんが、DeepMindのrepoには含まれています。人間による予想の形式化の重要性は、人間がLeanの主張が予想の背後にあるアイデアを忠実に捉えていることに同意すれば、（おそらくAI生成の）Leanコードが予想の証明または反証を構成しているかどうかを確認するのは些細なことだということです。Leventにおめでとう、Akhilが彼に問題を提案してくれたことに感謝し、DeepMindがすでに主張を形式化し、反例の形式的な検証を些細なことにしてくれたことに感謝します。

Jacobian予想は解決されました！すごい！この作業の次のステップは、人間が例で何が起こっているかを正確に理解することです。このような作業の真の価値は、人間に数学のより良い理解を与えることです。実際、AkhilはGrothendieckの反例を「ランダムな環のランダムな表示と、何かが機能しないことを示すランダムな計算」というよりもはるかに深い方法で理解しようと取り組んでいます。私たちに次に必要なのは、これらの extraordinary な例から引き出せる洞察です。

生きているって素晴らしい時代です。