Conwayの精密化予想の証明を「バイブス」で導き出した方法

要点

Dan Abramovは、Claude、ChatGPT、およびCodexエージェントを使用して、全能整数（omnific integers）に関するConwayの精密化予想の証明を生成、監査、およびLeanによる形式化を行いました。この証明は機械的なチェックには合格していますが、独立した専門家による検証はまだ完了していません。

Conwayの予想とは

Conwayの精密化予想は、全能整数の積の等式 (a b = c d) が成り立つ場合、以下の条件を満たす整数 (e,f,g,h) が存在すると主張するものです。

(a = e f)
(b = g h)
(c = e g)
(d = f h)

言い換えれば、全能整数の任意の2つの因数分解は共通の精密化を許容するということであり、積を素因数に分解して再構成できるという初等整数論の性質を反映しています。

AI駆動の研究パイプライン

1. 問題の選定

Claude に超現実数における未解決問題の選定を促しました。Claudeは、L’InnocenteとMantovaによる最近の研究を引用し、この予想を (K((\mathbb{R}^{\le 0}))) における既約元に関する命題に帰着させた上で、精密化予想を選択しました。
著者は、Claudeによる帰着が不完全であったことを指摘しつつも、ONAG（On Numbers and Games）の50周年という記念すべきタイミングであることから、この問題に取り組む意義を見出しました。

2. 初期のワンショット試行

最初のプロンプトではClaudeに「ブレイクスルーを起こせ」と指示しました。モデルは専門用語を多用した支離滅裂な文章を生成し、検証不可能でした。
ChatGPT（Sol と呼称）に切り替えたところ、より控えめな主張が得られましたが、依然として人間による広範な精査が必要でした。

3. マルチエージェント・ラボ（Codex）

プロジェクトマネージャー (PM) エージェントがワークフローを調整しました。
2つの 数学 (Math) エージェントが候補となる補題を生成しました。
レッド (Red) エージェントが欠陥の発見を試みました。
ランダム (Random) エージェントが周辺的なアイデアを探索しました。
Lean エージェントが有望な結果をLeanコードに翻訳しました。
エージェントは「カフェテリア」チャットルームを介して通信し、役割の境界を維持しながら相互作用を促進しました。

4. トークン消費量とコスト

約 400億トークン が処理され、そのうち約2億1000万トークンが出力されました。
推定APIコスト: ≈ 40,000ドル。

主要なマイルストーン

週	マイルストーン	結果
1	問題の枠組みと初期プロンプト	Claudeが曖昧な問題文を生成。ChatGPTが批判的な「懐疑的」な声を提供。
2	Codexエージェントによるラボ構築	数十のドラフト「論文」を生成。多くに造語や論理的欠落が含まれていた。
3	最初の行き詰まりと「ブートストラップ」証明の失敗	ChatGPTが完全な証明を主張したが、新しいセッションで循環論法が露呈。
4	誤字修正による正当性の確認	査読済み文献のモデルによる誤り発見が著者によって確認され、信頼性が向上。
5	破棄と救済戦略	ノイズの多いドラフトの大部分を破棄し、Hahn級数における有限次素数性に関する一貫した結果を保持。
6	形式検証	2つの独立したLeanエージェントが有限次の結果を証明し、後に完全な精密化予想を証明。
7	証明マップツール	カスタムスクリプトがMermaid図とインタラクティブなWeb UIを生成し、依存構造を可視化。

最終的なLean証明

証明はGitHubリポジトリ gaearon/conway‑refinement の ConwayRefinement/Standalone に格納されています。
各スタンドアロンファイルはMathlibのみをインポートし、自己完結性を確保しています。
監査による確認事項:
- 余分な公理が導入されていないこと。
- インポートがスタンドアロンポリシーに従っていること。
- すべての命題にペアとなるLean証明が存在すること。
Leanカーネルによってコンパイルされた証明証明書が、予想の命題を裏付けています（コンパイルの動画を参照）。

学んだ教訓

バイブス vs 理解 – プロジェクトは深い個人的専門知識なしに成功しましたが、ドリフトを検出するために絶え間ない「バイブスチェック」が必要でした。
エージェントの規律 – 背景の形式化と新しい結果の生成に別々のLeanエージェントを使用することで、安定したコードの汚染を防ぎました。
監査インフラ – スタンドアロンフォルダ、モジュール階層チェック、公理リンターは、査読者の信頼を得るために不可欠でした。
人間によるフィードバック – 数学者に誤字修正についてメールを送ることで、現実的なチェックと信頼性の足がかりが得られました。
モデルの補完性 – Claudeは構造化されたLean生成に優れ、ChatGPTは探索的な数学と批判において優れていました。
トークン経済 – よりガイドされたワークフローにより、コストを5〜10分の1に削減できる可能性があります。
証明の提示 – Leanコードを読みやすいPDFに翻訳することが依然としてボトルネックであり、インタラクティブな証明マップがそのギャップを埋めるのに役立ちました。

コミュニティの反応（HNコメントより抜粋）

「このアプローチは魔法使いと魔術師の違いのように感じられる。著者は呪文を完全に理解することなく、強力な存在（LLM）を召喚している。」 – @gbjcantab

「私は数学者ではないが、『すべての隙間にスポーンする』というルールは、どのようにして有理数を超えていくのか？」 – @rlue

「このワークフローは、複数のエージェント、敵対的テスト、継続的インテグレーションという現実世界のエンジニアリングプロセスを反映している。」 – @spongebobstoes

「証明は印象的だが、独立した検証がなければ数学コミュニティは懐疑的なままだろう。」 – @patcon (教授のレビューへのリンク付き)

未解決の問い

検証 – 独立した数学者がLeanコードを監査し、論理的なステップを確認する必要があります。
簡略化 – 現在の証明は長大です。将来的に生成された証明マップを使用して圧縮できる可能性があります。
一般化 – 同じマルチエージェントパイプラインを、ドメイン知識なしで他の未解決問題に適用できるでしょうか？
モデルのアライメント – LLMプロバイダーは、「幻覚」による定理を助長することなく、厳密な数学的研究をどのように支援できるでしょうか？

著者は、証明リポジトリおよびZulipチャンネルでの批判、バグ報告、議論を歓迎しています。