Knuthの「Claude Cycles」問題で人間・AI・証明支援系の協業が進展

 (twitter.com/BoWang87)
2 ポイント 投稿者 GN⁺ 2026-03-30 | 1件のコメント | WhatsAppで共有
  • Donald Knuthが提示したHamiltonian 分解問題の未解決部分が、人間とAIの協業によってさらに解決された
  • Claudeが奇数 m の解法を見つけ、「Claude’s Cycles」と命名され、その後11,502個の巡回のうち996個がすべての奇数 m に一般化された
  • Dr. Ho Boon SuanがGPT-5.4 Proで偶数 m≥8 に対する14ページの証明と m=2000 までの計算検証を実施
  • Dr. Keston Aquino-MichaelsはGPT と Claude のマルチエージェントワークフローで、奇数・偶数 m の両方に対する単純な構成法を発見
  • Dr. Kim MorrisonがLean 証明支援系で Knuth の解法を形式検証し、人間・AI・証明ツールの協業エコシステムが完成した

Claude’s Cycles 問題解決の拡張された協業

  • Donald Knuthが提示したHamiltonian 分解問題の未解決部分が、人間とAIの協業によって解決された
    • 当初はClaudeが約1時間の探索で奇数 mに対する解法を見つけ、Knuth はこれを**「Claude’s Cycles」**と命名した
  • その後の更新論文では、基礎事例 m=3の場合に正確に11,502個の Hamiltonian 巡回が存在し、そのうち996個がすべての奇数 m に一般化されることが示された
    • Knuth はこのうち760個の有効な「Claude 型」分解を確認した
  • 偶数 mの場合は Claude が完成できなかったが、Dr. Ho Boon SuanがGPT-5.4 Proを用いてm≥8に対する14ページの証明を作成し、m=2000 までの計算検証を行った
  • 続いてDr. Keston Aquino-Michaelsが、GPT と Claude を併用するマルチエージェントワークフローを通じて、奇数・偶数 m の両方に適用できる単純な構成法を発見した
  • Dr. Kim Morrisonは Knuth の奇数に対する解法をLean証明支援系で形式化して検証した
    • その結果、人間、複数のAIシステム、そして形式証明ツールが並行して協力する完全な数学的協業エコシステムが形成された
  • この一連の過程は、1つのAIによる単独の問題解決から出発し、複数AI・人間・証明支援系の協業へと拡張された新しい数学研究モデルを示している
  • 最新論文は Stanford CS Faculty のWebサイト(www-cs-faculty.stanford.edu/~knuth/papers/)で公開されている

関連記事

1件のコメント

 
GN⁺ 2026-03-30
Hacker Newsのコメント

  • 私は前から、AIはマクドナルドを運営する前にフィールズ賞を取ると言ってきた
    数学は人間にとって、ハンマーでネジを回すように難しく感じられる
    LLMは浅いが広い探索に強く、新しい数学的パターンを数多く発見している
    今後はLLMではなく、Lean構文木ベースのAlphaGo式強化学習へ移行すると予想している
    数学者が使う「10個のトリック」を潜在ベクトルとして符号化できれば勝負は決まる

    • トリックは結局、論理式のパターンにすぎない
      私たちは幾何学的類推を通じて代数幾何を数論の問題に適用するように考える
      Lean木で学習したAIは、人間よりも広い直観体系を持つかもしれない
      チェスでStockFishが示した事例のように、このアプローチは**機械論的解釈可能性(mechanistic interpretability)**の観点から研究する価値がある
    • 私は職業数学者だが、良い証明では問題の表現方法が核心だ
      トリックを取り出して使うこと自体は、LLMもすでに得意だ
      しかし問題を正しく表現する部分は依然として人間の役割であり、それは自然なことだ
    • もしシステムが自力で新しいトリックを発見するよう学習されたら、本当に驚くべきことだろう
    • 「AIはマクドナルドを運営する前にフィールズ賞を取る」という言い方がとても気に入った
      私はここに「最後に自動化される職業はQAだ」という自分版を付け加えたい
      今回の技術の波は知識労働の本質を改めて考えさせ、そのおかげで私たちはより鋭くなるだろう
    • 私もLean木ベースの強化学習アプローチを自分でプロトタイプ実装しようと、ゆっくり試している

  • 昔、4chanの格言である「trolls trolling trolls」を知って以来、インターネット上のやり取りを常に疑いの目で見るようになった
    Redditはすでに「死んだインターネット」になったと感じていたが、このスレッドを見ると、今では誰がボットで誰が人間なのか区別がつかない

    • その洞察は本当に重要だと思う
      だから私はRememberBuddyというサービスを作った — 日常の洞察を忘れないよう保存しておく場所だ

  • AI数学の進化は、90年代にGreg Eganが小説で予見した軌跡をたどる気がする
    数学の本質は変わらないが、なぜそれをやるのかは変わるだろう
    Eganの『Diaspora』では、数学的発見はまるで岩塩鉱山から宝石を掘り出す行為のように描かれている
    ある人は宝石そのものの純粋な美しさを、またある人は実用的価値を追求する
    現在のTerence Taoが設立した研究所のような場は、こうした未来に通じている
    短期的には、この種の研究はAIシステムの正確な情報生成能力を大きく向上させるだろう

  • 知識の発見は単に過去の行動を真似することだと考える人もいるが、私はそうは思わない

  • 専門家がモデルをうまく導けば、たいていの問題は解決できる
    モデルは専門家の面倒な作業を代行する道具としては優れているが、複雑な問題では依然として盲点がある

  • 論文でシステムプロンプトの一部を見たが、
    「すべてのexploreXX.py実行後、直ちにplan.mdを更新せよ」というルールがあった
    こうしたプロンプトが高度な問題解決性能を向上させる理由が気になる

    • おそらく、過程を失わずに再開しやすくするための仕掛けなのだろう

  • 私たちはますます、OpenAI CEOのいう**「サブスクリプションとしての知能(intelligence as a subscription)」**というビジョンに近づいている

  • タブ切り替えを減らすことは過小評価されている
    AIツールの半分はUXの問題ではなく、モデルアクセスの安定性確保をめぐる戦いだ

  • 「100匹のサルに100丁の銃と建築資材を与えたら、家を建てるのか、それとも銀行を襲うのか？」
    その結果が出たなら、それが意図された行動なのかを問いかけたい

  • このツイートを見たが

    • コメントの大半が明らかにAIが生成した文のパターンに見えた — 「それはXではなくYだ」という反復だ