人間の数学者、反例探しでAIに追い抜かれる

 (xenaproject.wordpress.com)
2 ポイント 投稿者 GN⁺ 5 시간 전 | 1件のコメント | WhatsAppで共有
  • ChatGPTとClaude系モデルが、わずか数週間のうちにエルデシュの単位距離予想、グロタンディークの群スキームに関する問い、Jacobian Conjectureに対する反例を作り、一部はLeanで検証された
  • OpenAIのSolは、エルデシュの反例と必要な大域類体論の結果を3週間で120万行のLeanコードとして形式化した。これは9年かけて書かれたmathlibの230万行の半分を超える規模である
  • グロタンディークの60年来の問いに対して、Solは12ページの反例を見つけ、Fableが4時間で1,076行に形式化し、位数4だが4によって消滅しない群スキームの存在を確認した
  • 自動形式化は研究速度も大きく引き上げ、Andrew Yangは約2週間で25万行のLeanコードを書き、フェルマーの最終定理に必要なモジュラリティ持ち上げ定理プロジェクトを事実上完成させた
  • AIが生成した非形式的な数学をそのまま信頼することはできないが、予想を正確なLean命題にすれば、証明と反証を機械的に検査できる。人間は反例からより深い数学的洞察を引き出す必要がある

エルデシュの単位距離予想と大域類体論

  • 2026年5月20日、ChatGPTが離散幾何学のエルデシュの単位距離予想を反証した
    • 1960年代のGolodとShafarevichによる深い整数論の定理を用いて反例を構成した
    • 複数の数学者が事前に論証を検討し、妥当だと判断したが、発表時点ではLeanによる形式化はなかった
  • 5月26日、フィールズ賞受賞者でLogical Intelligenceの最高科学責任者であるMike Freedmanが、自社システムでChatGPTの論文全体をLeanに自動形式化したと報告した
    • 形式化された範囲は、Golod–Shafarevichの定理がエルデシュの反例を含意するという命題だった
    • 基礎となる整数論の定理そのものには100ページ以上が必要で、大域類体論の膨大な部分に依存している
  • 2025年の類体論形式化サマースクール以降の1年間で局所的な場合はほぼ完成したが、大域的な場合は未解決のままだった

Solが作った120万行の完全な形式化

  • 6月26日、OpenAIのBoris Alexeevが新モデルSolを誘導し、数学の公理以外は何も仮定しないエルデシュの反例の完全な形式化を作ったとLean Zulipで公開した
  • Solは3週間で120万行のLeanコードを生成した
    • 9年にわたって書かれたmathlibは230万行である
    • コード品質にはばらつきがあったが、大域類体論の難しい結果と、数体のコホモロジーに関する非自明な定理を実際に証明した
  • Leanは任意のコマンドを実行できるプログラミング言語でもあるため、悪性コードの可能性を考慮して、生成コードはサンドボックス内で実行した
  • この規模と速度は、大規模なAI生成数学開発が避けられないという判断につながった

Formalizing Fermatワークショップとツールへのアクセス

  • 7月6〜10日に開催されたFormalizing Fermatワークショップには25人が参加したが、スポンサーのLogos Researchの自動形式化システムは同時に5人しか利用できなかった
  • 全参加者に1か月分のClaude Maxサブスクリプションを提供し、Claude Fableを使えるようにした。OpenAIも1か月分のChatGPT Proアクセス権を無料で提供した
    • Solは7月9日にリリース予定だった
    • Fableは7月7日に終了予定だったが、実際のアクセスは維持された
    • 参加者はワークショップ5日間のうち4日間はSolとFableを、全期間にわたってLogosのツールを利用できた
  • フェルマーの最終定理の形式化に必要な有限平坦群スキーム理論を開発するため、古典的な論文をFableとChatGPTに入力し、自然言語の解説を書かせた
    • Logosは、その解説に含まれるある命題が偽であることを見つけ、明示的な反例を示した
    • 確認の結果、標準的な構成を記述したLLM生成文書が誤っており、人間は読む過程でその誤りを見落としていた
    • 単に論証を理解できないと答える代わりに、論証が誤っていることの証明を提供した点が異なっていた

グロタンディークの群スキームに関する問い

  • シカゴ大学教授のAkhil Mathewは、位数(n)のすべての有限自由群スキームが(n)によって消滅するかを問う、グロタンディークの古い問いをAIに提示した
    • Deligneは可換の場合を証明した
    • グロタンディークは基底空間が被約である場合を証明した
    • Rene Schoofがさらに多くのケースを扱い、Emiliano Tortiも前年の論文でより一般的な場合を証明していた
  • ワークショップ翌日の7月11日、Solが反例を見つけ、12ページのPDFを生成した
    • 非形式的な結果ではなく全体のLean形式化を求めると、Fableが4時間で1,076行に自動形式化した
  • Leanファイルにファイル削除のようなコマンドがなく、定理だけが含まれていることをまず確認したうえで、ノートPCでコンパイルした
    • 命題にmathlibの概念だけが使われているかを確認した
    • 命題が実際に反例の存在を表しているかを点検した
    • 証明が正常にコンパイルされるかを検査した
    • 全体の検証に5分もかからなかった
  • 検証の結果、位数4だが4によって消滅しない群スキームが存在することが分かった
  • Akhil Mathewはこの反例をmathlib PRとして提出した
  • エルデシュの反例は約100万行だった一方、グロタンディークの反例は約1,000行とはるかに単純だったが、60年来の代数幾何学の問いを機械が解決した事例となった

専門家の反応とモジュラリティ持ち上げ定理

  • 7月14日、Imperial Collegeのある教授は、グロタンディークの反例が容易に発見された事実は、人間がその問題について十分長く考えてこなかったことを示すだけだと評価した
  • 博士課程学生のAndrew Yangは、フェルマーの最終定理に重要なモジュラリティ持ち上げ定理をLeanで形式化する際にSolとFableを使った
    • 約2週間で25万行のLeanコードを書いた
    • これによりプロジェクトを事実上完成させた
  • Imperialの別の教授は、大学院生がSolとFableに月200ドルを支払うことを理解しがたいと見ていたが、この成果を確認した後は、むしろツールに月200ドルを使わない博士課程学生のほうが非合理的だと判断した
  • Harvardはすでに、すべての博士課程学生、ポスドク、教授にFableの無料アクセス権を提供していた

Jacobian Conjectureの反例

  • Akhil MathewとLevent Alpögeは、代数幾何学で追加の反例を探す方法を議論し、Fableが約100年にわたって未解決だった有名問題Jacobian Conjectureの反例を見つけた
  • Levent Alpögeは、2026年ワールドカップ決勝の最中に解決されたと思われる結果をXで公開した
  • Akhil Mathewが新しいmathlib PRを提案した時点では、Paul Lezeauがすでに反例を手動で形式化し、DeepMindのFormal ConjecturesリポジトリにPRを提出していた
  • mathlibには数学的予想の大規模な一覧はないが、Formal Conjecturesリポジトリにはそれがある
  • 人間が予想の意味を忠実に表すLean命題に合意すれば、AIが生成したコードがその予想を証明または反証しているかを確認する作業は簡単になる

形式検証後に人間に残された課題

  • Jacobian Conjectureでは、人間がその反例で正確に何が起きているのかを理解する作業が次の段階である
  • グロタンディークの反例についても、任意の環表示と計算を列挙する水準を超えて、より深く理解しようとする作業が進んでいる
  • 反例の価値は、問題を形式的に終わらせることにとどまらない。人間が数学をよりよく理解できるように洞察を抽出する過程で完成する

関連記事

1件のコメント

 
GN⁺ 5 시간 전
Hacker Newsのコメント

  • 大学院時代、指導教員の研究授業で未解決問題に直接貢献する機会があった。ある金曜日、教授は真であってほしい滑らかで美しい予想を提示したが、奇妙な例外が好きで証明の道具も足りなかった私は反例探しに集中し、1時間で見つけた。
    教授は週末いっぱい証明に失敗したのだが、異なる道具・期待・動機を持つ人が同じ問題を見ると、まったく別の方向から貢献できることを示す出来事だった。偉大な指導教員に比べるべくもなかったが、その時だけは別の方向を見る理由があり、それが私の唯一の数学研究への貢献である小さな反例につながった。

    • 機械が反例探しに強い理由もここにありそうだ。予想に対する美的な執着もなく、醜い結果を出すことに恥じらいもない。
    • 数学者としての私の実感は逆だ。証明は知っている証明を少し変形すればよいが、反例を作るには対象の構造を深く理解する必要があり、自分の能力を超えることが多い。
      ただし、これは私が理解しにくい抽象的対象を主に扱っているからかもしれず、数や多項式では逆である可能性が高い。
    • 学生にまだ解けていない問題を公開し、参加を促す教授・研究者・教師はもっと高く評価されるべきだ。大学最初の工学の授業で講師が1年生たちに「私たちがまだ解けていない問題なので、アイデアが浮かんだら知らせてほしい」と言った時、かつてないほど歓迎され、共同体に迎え入れられたと感じ、退屈になりかねない学業の初期に大きな刺激を受けた。
    • 『How to Solve It』にもほぼ同じ話がある。
    • さらに極端で、逆方向のZeemanの逸話がある。彼は5次元空間で結び目になった球を探すために何年も費やしたが、それが不可能だと気づき、数時間で証明した。
      https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

  • 双子素数予想で有名なYitang Zhangは、PurdueでTzuong-Tsieng Mohの指導を受けながらヤコビアン予想を7年間研究した。博士論文の核心的段階がMohの誤った系に依存していたことが判明し、Mohは推薦状の執筆を拒否、Zhangは教育・研究職を得られず、数年間Subwayで働くことになった。
    1986年に研究を始めた時にChatGPTがあったらどうだったのか気になる。今では感動的な成功談になっているが、「庾信の生涯はこの上なく寂寥たるものだったが、晩年の詩賦は江関を揺るがした」という詩句のように、複雑な感情を呼び起こす。

    • 数学の博士号発表中に、審査教員が証明の欠陥を見つけたことがある。学生が理解した後で「では、どうすればいいのでしょうか？」と尋ねると、審査教員はただ肩をすくめただけだった。
    • 後に双子素数予想で成功したので感動的と言えるかもしれないが、学界のこうした話にはうんざりしている。政治と評判管理が多すぎ、Zhangはそのような苦痛を味わうべきではなかった。
      数学方面へ研究を広げる中で、文献中の命題のかなり多くが偽であり、応用分野の文献にまで広く伝播していることに驚いた。問題を知らせても、Zhangの逸話のように防御と否認で応じる場合が多い。LLMは証明に有用だが大きく間違うこともあり、別の直観で探索の方向を提案するもう一人の人間に近いので、1986年でも結果は同じだったように思う。
    • ChatGPTが訳した詩の意味は「Yu Xinの人生は徹底して寂しかったが、晩年の詩と賦が江湖を揺るがした」くらいだ。

  • 数学において反例は、定義を磨き、証明を鋭くするうえで非常に重要だ。Imre Lakatosの1976年の著書『Proofs and Refutations』を勧める。位相幾何学・確率論・解析学などには、反例だけを扱った本もかなり多い。
    https://en.wikipedia.org/wiki/Proofs_and_Refutations
    https://www.amazon.com/s?k=counterexamples

  • 反例を見つければ、偽である命題を証明しようとして時間を浪費せず、別の問題に移れるので、少なくとも数学では人類の時間をより生産的に使えるようにしてくれる。

    • 反例による反証は効果的だが、究極的には満足できるものではない。答えは与えてくれるが、数学がなぜそのように機能するのかを理解させたり、新しい問いへ導いたりはしない。
      何が優雅で洞察に富む証明なのかを人間が判断している間は、人間の数学者の仕事は残るだろう。
    • 反例は定理の命題を洗練するうえでも有用だ。理論計算機科学の研究では、真であってほしい定理を証明しようとして反例を見つけ、命題を修正して続ける過程がよくある。
      計算機科学の多くの定理が帰納的・余帰納的定義を扱う点も役に立っている。
    • 特に反例が形式検証されているなら、何年にもわたる推測的な努力を、ほぼ即座に確定的な答えへ変えてくれる。
    • しかし全体として時間がより生産的に使われたと断定することはできない。命題を証明するにせよ反証するにせよ、最終的に真であれ偽であれ、その過程で新たな洞察が生まれることがある。

  • 数学版『ジョン・ヘンリーのバラッド』もAIが書くことになりそうだ。機械でさえ上回れない、「THE BOOKに載るような」証明を出す最後の人間チャンピオンが誰になるのか気になる。
    https://en.wikipedia.org/wiki/John_Henry_(folklore)
    https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

    • これはサッカーファンのように数学を競争として見る、不健全な見方だ。数学で最も価値があるのは美しい証明だけでなく、有用な定義であり、良い定義とそこから良い予想を作ることは、LLMがまだ征服しようとしていない領域だ。
    • まだそれほど劇的ではないが、まもなくその段階に到達する可能性はある。AIの能力が漸近的に発展するのか加速するのかを構造的に予測する根拠はなく、どの問題が新しい方法で解かれるのかについても、両方の可能性が開かれている。
      AI能力の内部と成長曲線を私たちは理解しておらず、意図的に性能を低く見せているのかどうかすら正確には分からない。測定に抵抗する創発現象かもしれないし、数年後には時計のように予測可能になるかもしれない。知っている人はおらず、いたとしても語らないし、声の大きい人たちも何も分かっていない。

  • 大学院生の有意義な成果を大きく早められるなら、学生1人あたり年間2,400ドルを投資しない理由はない。全体の費用から見れば小銭に近い

    • 一部の大学院生は、自分を「有意義な結果を生産する機械」ではなく倫理的存在だと見ている。有用なLLMでも、盗用された学習データと莫大な環境影響のために正当化しにくいことは誰もが知っている
    • EPSRC博士課程の生活費奨学金は約20,000ポンドなので、年間費用の約10%に相当する。学生個人にとっては大きな負担である

  • 大学時代にLLMが作ったLean形式化があればよかった。講義スライドの数学には誤りが多く、一部の教授は「証明はスライドにある」と説明要求を拒みながら、誤りを認めることにも消極的だった
    Leanの証明そのものは理解に適していない場合が多いが、それを基に人間が理解しやすい論証を生成できるようになることを期待している

    • 最初の主張には同意しにくい。学習曲線は急だが、よく書かれたLean・Agda・Rocqの形式化は証明を理解するうえで非常に優れている。良い形式化は概要と核心的な論証を構造的に示し、紙の証明と違って望む深さまで全ステップの詳細を確認できる
      Martín EscardóのTypeTopology Agdaリポジトリが良い例だ。一方、現在LLMが生成した形式化は非常に雑然としていることがあり、真であることを認証し興味深い論証を含んでいても、数学的理解を高める形に整えるには相当な作業が必要になる。対話型Agdaチュートリアルはlets-play-agda.quasicoherent.ioにある
    • 形式化は、論争を終わらせ疑念を完全に取り除くライプニッツ的アプローチにも使える

  • 数学者にとって反例は、物理科学における予想外の結果のように、当面は厄介でもモデルの不正確さを明らかにするため極めて重要になり得るものなのか、それともプログラミングのバグ報告のように些細で面倒な細部なのか気になる

    • 反例は条件の役割を明確にしてくれる。証明の各条件を破ったときに何が失敗するのかを示す、最も単純で覚えやすい反例があると非常に有用だ
      数学者は頭の中に反例動物園を持ち歩く傾向がある。定理を復元するときも、鋭く記憶に残る反例を思い出し、それらを排除するように定義域や条件を絞ることができる
    • 『Counterexamples in Topology』や『Counterexamples in Analysis』のように、反例を通じて分野の微妙な違いを教える教材がある。意図された正常な対象だけを学ぶより、病理的・退化した例から細部を学びやすいため人気がある

  • この数学のかなりの部分は理解が難しいが、概ね定理証明を扱っているようだ。AI数学が加速し続ければ、将来工学や生物医学に応用される新しい数学まで発見するのか、人類は巨大なブレークスルーの直前にいるのか、それとも既知のものを証明するにとどまるのか気になる

    • 可能性はある。圧縮センシングは生物医学に応用される新しい数学の例と見なせ、MRIの撮影時間を大幅に短縮して患者体験を改善し、より多くの患者が検査を受けられるようにできる
      https://en.wikipedia.org/wiki/Compressed_sensing
    • 工学や生物医学への応用はおそらく長期的な話だとしても、新しい数学的方法の発展は基礎物理学研究ではより早く重要になる可能性がある。宇宙モデルの表現や検証を可能にした数学ツールが登場し、モデルが大きく改善されたことはしばしばある
    • 可能だとしても非常に長い時間がかかるだろう。ほとんどの応用分野では、数百年前の数学でさえ、ようやく本格的に活用し始めた程度である

  • いつか数学者が検討すべき証明に埋もれ、過信された偽の命題が数学界に入り込むかもしれない。未来の数学者は、AIを使うソフトウェアエンジニアのようにAI生成の証明数千行を検査し、微妙な誤りを探すことになるのかもしれない

    • その時点はすでにずっと前に来ている。今日の文献は膨大で誤った証明に満ちており、出版済みの結果の中にも数は分からないが確実にゼロではないだけの偽の結果が混じっている