エルデシュ問題のウェブサイトでAI支援が日常化しつつある

 (mathstodon.xyz)
1 ポイント 投稿者 GN⁺ 2025-11-25 | 1件のコメント | WhatsAppで共有
  • エルデシュ問題 #367 の解決過程で AIツールが中核的な役割 を果たし、人間の数学者と協働する事例が報告された
  • Wouter van Doorn が問題の第2部に対する 人間が作成した反例 を提示し、その後 Gemini Deepthink が関連する合同式の完全な証明を生成
  • Terence Tao は Gemini の p進代数的整数論に基づく証明 をより単純な形に変換して公開し、その後 Lean での形式化可能性 に言及
  • Boris Alexeev は Harmonic の Aristotle ツール を用いて Lean 形式化を完了し、AIの悪用防止のため最終命題は手動で検証
  • この一連の過程は、数学研究においてAI補助が徐々に標準的手順として定着しつつある ことを示している

エルデシュ問題 #367におけるAI協働の事例

  • 11月20日、Wouter van Doorn が問題の第2部に対する反例を提示し、これは特定の合同式が真であるという仮定に依存していた
    • 彼はその合同式の妥当性を他の参加者に検証してほしいと求めた
  • 数時間後、Terence Tao はこの問題を Gemini Deepthink に提示し、約10分で合同式の完全な証明と全体の論証確認を得た
    • Gemini の証明は p進代数的整数論 を用いており、Tao はそれをより単純な初等的証明に変換してサイトに掲載した
    • Tao はこの証明が Leanで「vibe formalizing」 可能だろうと述べた

Lean 形式化と検証

  • 2日後、Boris Alexeev が Harmonic の Aristotle ツール を使って Lean 形式化を完了した
    • AIの誤用を防ぐため、最終命題は手作業で直接形式化した
    • 全工程には約2〜3時間を要し、成果物はオンラインで公開された
  • Tao はその後、AIを用いた 文献検索 も行ったが、関連研究はいくつかあったものの、問題 #367 に直接関係するものは見つからなかった

コミュニティの反応と議論

  • 一部のユーザーは Tao の更新を通じて、AIの学術数学への活用状況 を興味深く見守っている
  • 別のユーザーは Lean の形式主義的アプローチ に批判的な見解を示し、数学的理解は圧縮（compression）なのに対し、Lean はそれを 低レベルな詳細へ分解する（decompression） と指摘した
    • 関連文書 “Against Lean: Why Proof Assistants Formalize the Wrong Thing” では、Lean のような証明支援系が数学の本質を誤って捉えていると主張している
  • また別のユーザーは AI対話の正確性の問題に触れつつ、細かな調整は必要だが使っていて楽しい と評価した

関連記事

1件のコメント

 
GN⁺ 2025-11-25
Hacker Newsのコメント

  • 数学寄りのML論文をAIアシスタントに投げて、簡単な説明や疑似コードにして返してもらえるのは驚くべき体験だ
    大学で学んだことを25年以上ほとんど使ったことがなかった自分にとって、本当に大きな助けになっている

    • その説明が正確かどうかをどう検証するのか気になる。数学的定義にはとても微妙な部分が多い
    • こういう点こそ、LLMが学習で真価を発揮する部分だと思う
      論文をClaudeに入れて概要を受け取り、その後で質問を続けられる
      学士や修士のときに学ばなかった生物学のような分野でも、知識のあるチューターと対話するように深く掘り下げられた
    • 数学の記法は文脈依存性が高いので、LLMにLispのような低文脈言語に変換してもらうと、構造をはるかに速く把握できる

  • 研究者や企業が科学研究でさらに大きな生産性向上を得られるようになってほしい
    完璧でないアシスタントでも、十分にレバレッジを高めてくれる

    • Taoが言及していたiOS向けの形式化アプリのベータ版がある → Aristotle
      Robinhood CEOが創業したスタートアップらしい

  • 「Vibe formalizing」は、「vibe engineering」や「vibe coding」の論理的な拡張のように感じられる
    問題の断片どうしがうまく噛み合わないとき、非形式的な方法と数学的厳密さを組み合わせる「Move 37 as a Service」のようなアプローチは興味深い

    • 以前、polyhedral compilationの論文を読んでいて行き詰まった箇所があったが、ChatGPTがreasoningの過程をうまく導いてくれた
      もちろん間違っている部分もあったが、自分の混乱を反映しながら対話できたので理解を深められた
      AIはユーザーの混乱している地点を把握するのがとりわけ得意だ

  • ハンガリーの数学者Erdősの名前の発音の話を聞いた
    ハンガリー語は綴りと発音がほぼ一致するが、人名では例外がある
    英語風にはだいたい「airdish」のように聞こえるらしい

    • Őは単にœ(oe)の音だ。ハンガリー人名の-yは、貴族の血統を意味していた**-i語尾の名残だ
      例: Görgey, Széchényi, Lánczos
      ハンガリー式の名前の順番は日本と同じ      姓-名(big endian)**順だ。例: 「Erdős Pál」「Neumann János」
    • 1960年に数学科の掲示板で見たユーモア詩があった — Erdosが書いた論文が**『円は丸い』定理を反証した**という冗談だった
    • 言語ごとに**発音記号(発音符号)**の意味が違うので、ハンガリー式の符号を英語の文にそのまま持ち込むのは不自然だと思う
    • 最初は「airdish」という発音が変に思えたが、「os」の語尾を**硬口蓋化(palatalize)**してみると、それらしく聞こえた
    • 自分はアメリカ人ではないからか、こういう発音の問題を気にする人は誰もいないように思える

  • コメントの中にanti-Lean寄りの反応があるのは興味深い

    • 数学者ではないが、その反Lean資料が信頼できるのか気になる
      単に別のアプローチを宣伝しているだけなのか、それとも哲学的にLeanに反対しているのか知りたい
    • Taoのような有名人は、変わり者や陰謀論者の関心を集めがちだ

  • 研究数学でAIを使ってみた結果は入り混じっている
    自明でない論証を自動補完してくれることもあるが、ある種の領域では完全に道を見失う
    まだAIは数学者を置き換えるというより、補助ツールとしてのみ有用な段階だと思う

    • 自分も似た経験がある。論文で単純な順列計算の問題をやらせたが、自分で解くより時間がかかった
      コーディングでも些細なバグを捕まえられないことがあったが、複雑な作業では大いに助けられた
      結局、これらのツールが専門家を置き換えるにはまだほど遠く、誇大宣伝はむしろ信頼を損なう可能性がある
      「月を約束したなら月を渡さなければならない」という言葉のように、現実的な期待値が重要だ

  • 生きているうちに、スタートレックのように「コンピューター、この数学の問題の証明を描いてくれ」と言える時代が来るとは信じがたい
    「Beam me up Scotty」もできたらいいのに

    • でも、そのたびに死ぬかもしれないなら、それはちょっと困る

  • 今夜、運転中にChatGPTとLLVMとGCCのパイプラインスケジューラの細かな構造について会話した
    そのおかげで生産性が大きく向上し、実験中のコンパイラ関連ノートも自動で整理してくれた
    以前なら想像もできなかったことだ

    • 自分の経験では、LLMは細部の一部を間違えている可能性が高い
      もちろん、人によって結果は異なるだろう

  • AIにErdosと名付ければ、みんなのErdos numberが1になりそうだ

    • あるいはDR-DOSの後継製品のようにも聞こえる
    • 実際にAI統合IDEのErdosという製品が存在する

  • 彼が既存のフロンティアツールをうまく活用して、協調的な数学研究環境を作り上げている点は印象的だ

    • 幸い、数学は偶像化や人気争いが結果の真偽を決める分野ではない
      その意味で、数学は今なお疑似科学的な影響力から自由な数少ない学問だと思う