2026年7月20日、インペリアル・カレッジ・ロンドンの数学教授 Kevin Buzzard がブログに、同業者を直撃する率直な一文を綴った：人間の数学者は「反例」で追い越されつつある。 理由は、AIがわずか2ヶ月の間に、数十年にわたって未解決だった3つの数学予想を連続して覆したからだ——そのうちの1つは約1世紀にわたって未解決だった。
Buzzard 自身はこう語る：「60年来未解決だった代数幾何の反例を検証するのに、5分もかかりませんでした。LeanのコードをノートPCにダウンロードしてコンパイルし、うなずいて『そうだ、これは確かに反例だ』と言っただけです。」
5分。これが人間の数学とAIの数学の境界線だ。本稿では、この境界線がいつ引かれ、何を意味するのかを考察する。
反例：証明よりも鋭い刃
まず基本的な概念を説明しよう。数学において、命題が真であることを証明するのは非常に難しい——全てのステップが厳密で、一つの誤りも許されない緻密な導出を書かねばならない。しかし命題が偽であることを示すのは、比較的「簡単」だ：反例——全ての前提条件を満たしながら結論を満たさない具体的な構成——を1つ見つければよい。
「全ての白鳥は白い」と言う人がいたら、世界中の白鳥をすべて調べる必要はない。1羽の黒い白鳥を見つければ十分だ。
1つの反例があれば、数学者の生涯の研究を終わらせることができる。だからこそ反例は数学史において創造的な役割を果たしてきた——理論の限界を明らかにし、数学者に仮定の再考、定義の改善、理論の前進を迫る。ある意味では、反例は数学進歩の燃料である。
AIはこの「黒い白鳥探し」の技術を、想像を絶するスケールへと押し上げている。
2026年5月〜7月：AIの3連撃
時系列に沿って、この3ヶ月間に何が起きたのかを整理する。
第1撃：Erdősの単位距離予想（1946年提唱、2026年5月20日に崩れる）
伝説的な数学者 Paul Erdős が1946年に提起した離散幾何の問題。ChatGPT が反例の構成を与えた。Buzzard の第一声は「Leanで検証したのか？」だった。していなかった。しかし1週間も経たないうちに、フィールズ賞受賞者の Mike Freedman（現 AI企業 Logical Intelligence の最高科学責任者）からメールが届く——彼らのシステムがこの論証を自動でLeanコードに変換したという。
1ヶ月後、OpenAI の Boris Alexeev が新モデル Sol を使ってさらに徹底的な作業を完了：数学の公理から出発し、反例全体を完全に形式化した。Sol はこのために120万行のLeanコードを生成した。
比較すると、Lean コミュニティが9年かけて書いた中核数学ライブラリ mathlib は、合計230万行だ。AI が3週間で生成した量は、人間の9年の蓄積の半分を超えた。Buzzard の評は簡潔だ：「大規模AI生成による数学の発展はもはや不可避である。」
第2撃：Grothendieckの群スキーム問題（1960年代提唱、2026年7月11日に崩れる）
Grothendieck は20世紀最大の数学者の一人だ。60年前に彼は問いを立てた：n次の有限自由群スキームは必ず n で消えるのか？Deligne は可換な場合を証明し、Grothendieck 自身は底環が既約な場合を証明した——しかし完全な結論は未解決のままだった。
Sol が反例を見つけた。証明全体はわずか1076行のLeanコードである。Buzzard は5分足らずで全ての検証を通過させた。彼は数学者 Akhil Mathew に数学ライブラリへのこの反例の提出を勧めた——そして冗談めかして「次はホッジ予想に挑戦してみるか？」と付け加えた。
第3撃：ヤコビアン予想（1939年提唱、2026年7月19日に崩れる）
これが最も衝撃的な一撃だ。ヤコビアン予想（Jacobian Conjecture）は多項式写像の逆問題である：多項式写像のヤコビ行列式が非零定数なら、その写像は必ず可逆か？この問題は1939年から未解決で、代数幾何学において最も魅力的でありながら最も頑固な予想の1つとされてきた。
今回反例を見つけたのは Anthropic の Claude Fable だ。2026年のワールドカップ決勝戦の最中に、反例を発見した。翌日、現代最も尊敬される数学者の一人であるテレンス・タオが詳細なブログ記事を公開し、この反例の数学的意味を「消化」した。
タオの計算によれば、この反例は3変数・最高7次の多項式写像である。そのヤコビ行列式は -2——非零定数の条件を満たす——だが、この写像は3つの異なる入力点を同一の出力点に写しており、1対1対応ではないため可逆ではない。さらに驚くべきことに、AI は120個の調整可能なパラメータを用いて、ヤコビ行列式に理論上現れうる1329個の係数を制御し、全ての非零項をちょうど相殺させた。タオの言葉を借りれば：「これは巨大な奇跡のように見える。」
Lean + LLM：創造性と確証の融合
ここで技術的なロジックを整理しよう。
Lean は「数学コンパイラ」である。Lean で数学の証明を書くと、全ての推論が厳密な型検査を通過しなければならない。「自明なステップは省略」は許されない——全ての「自明」を原子レベルまで展開する必要がある。コードがコンパイルを通れば、その証明は数学的に絶対に正しい——いかなる人間の判定者の信頼にも依存しない。
LLM（大規模言語モデル）は「構想」を担当し、Lean は「判定」を担当する。LLM が数学で抱える固有の弱点は「もっともらしい嘘」をつくことだ——本当は知らなくても、それらしい推論をでっち上げる。Lean の介入はこの問題を根本的に解決する：LLM が Lean コードを生成し、コンパイラが即座にチェックする。コンパイルが通らなければ、LLM はエラーメッセージを受け取って修正する。この反復をコンパイルが通るまで続ける——この時点で、AI が生成した数学的結果には厳密な正当性が保証される。
2026年3月、『Learning to Disprove』と題された論文がこの方法論を体系的に解説した。中核となる洞察は、LLM に命題を「証明」させる（嘘をつきやすい）よりも「反例」を探させる方が効果的だということだ——反例は一旦 Lean でコンパイルが通れば、動かぬ証拠となる。論文の著者らは「記号変異」戦略を採用し、既存の定理から特定の条件を系統的に削除することで、反例探索のための訓練データを大量に生成し、マルチリワード機構で LLM を訓練した。実験結果は、反例生成タスクにおいて LLM の精度が49%向上したことを示している。
これが「反例による超越」の技術的基盤だ：LLM が創造性を担当し、Lean が確証を担当し、人間の数学者は少なくとも結果の検証というフェーズでは観客になった。
数学界の「悲しみの5段階」
Buzzard はブログ記事で、周囲の数学者の反応を率直に記録している。インペリアル・カレッジでの昼食時に同僚から聞いた言葉：「反例がそんなに簡単に見つかるなら、人間が十分に時間をかけて考えていなかっただけだ。」彼は内心で苦笑した——彼自身、この「時間をかける価値がない」問題に丸々1週間を費やしたことがあるのだ。
これは典型的な否認の段階だ。
次に来たのは取引の段階。ある教授が驚きのメールを送ってきた：なぜ大学院生が月額200ドルも払って Sol や Fable を購読するのか？Buzzard の返答は単刀直入だった：「この200ドルを払わない博士課程の学生こそ非合理だ。」ハーバード大学は既に全数学博士課程学生、博士研究員、教員に Fable の無料アクセスを提供している。
感情的に受け入れられるかどうかは別として、1つの事実は明らかだ：数学研究において、AIツールを使いこなす者とそうでない者の間の能力差は、月単位で拡大している。
タオが示した方向性
全ての反応の中で、タオの姿勢は最も注目に値する。彼はAIの能力の限界を疑うことも、「これが数学と言えるのか」という哲学的な議論に陥ることもせず、腰を据えて詳細なブログ記事を書き、多項式の重み付き斉次性を計算し、幾何学的視点からの再構築を示し、さらには GPT-5 との議論の完全な会話ログまで公開した。
これは典型的な第一線の数学者の態度だ：成果はそこにある、まず理解し、そして活用する。
タオは HN での議論の中で次のように指摘している：「これは、一見不可能に見える数学的構成が、十分に大きな探索空間の中では見つけられるということを示している。」この言葉に隠された重要なメッセージは——探索空間は巨大だが、AI が探索の方法を教えてくれた。そしてこれはまだ始まりに過ぎない。
数学者に残されるものは？
AI が反例を見つけ、証明を検証し、完全な理論を自動形式化できるようになったとき、数学者に何が残るのか？
Buzzard の答えはこうだ：理解と解釈。 彼は言う：「これらの非凡な例の真の価値は、人間に数学のより深い理解をもたらすことにある。」Akhil Mathew は既に、Grothendieck の反例の背後にある構造をより深く理解しようと試みている——「ここで実際に何が起きているのか」を問い、「これはランダムな構成と偶然の計算に過ぎない」という水準にとどまるのではなく。
AI は「それは成立しない」と教えることはできるが、往々にして「それが我々の数学の図景にとって何を意味するのか」を教えることはできない。
歴史的に、数学者は繰り返し「計算」を機械に外部委託し、より高次の「理解」と「構成」に集中してきた。今や「反例探し」と「証明の検証」も外部委託できるようになった。残された人間の仕事は、まさに数学の最も中核的な部分かもしれない：機械が反例を机の上に並べたとき、それがなぜ重要なのかを本当に理解し、そこから何を学ぶかを見出すこと。
これは数学の終わりではない。しかし数学者の役割は、確実に不可逆的な進化を遂げている。
参考リンク：
- Xenaproject —— Kevin Buzzard の原著ブログ「人間の数学者が反例で追い越されつつある」
- HN ディスカッション（id: 48998362）—— タオのヤコビアン予想ブログを巡るコミュニティ議論
- Lobsters ディスカッション（s/wfmpqr）—— 技術コミュニティによるAI数学反例への深いコメント
- Terry Tao のブログ —— ヤコビアン予想反例の消化と数学的再構築
- SBSeminar —— ヤコビアン予想の新反例に関する数学的詳細の議論
- arXiv 2603.19514 —— Learning to Disprove：大規模言語モデルによる形式的反例生成
- ニュー・サイエンティスト誌報道 —— AI による87年越しの数学难题への解答
- GitHub DeepMind Formal Conjectures —— 形式化予想リポジトリ、ヤコビアン反例を収録
