AIとLeanを使ってConwayの精密化予想の証明を「ノリで」導き出した方法

TL;DR

私はマルチエージェントAIラボを構築し、数ヶ月にわたるプロンプトエンジニアリング、膨大なトークンを消費する実験、そしてLeanによる形式化を経て、全能整数（omnific integers）に関するConwayの精密化予想の機械的に検証された証明を生成しました。この証明はPalomarレジストリを通過し、非公式な専門家によるレビューも受けていますが、まだ独立した検証は完了していません。

Conwayの精密化予想とは

Conwayの予想（1976年）は、超現実数ツリーの整数部分である全能整数に関するものです。これは精密化特性を主張するものです。全能整数 $a,b,c,d$ に対して $ab = cd$ が成り立つならば、以下の条件を満たす全能整数 $e,f,g,h$ が存在する。

[ a = ef,\quad b = gh,\quad c = eg,\quad d = fh. ]

通常の整数ではこれは自明ですが（例：$210 = 10\cdot21 = 6\cdot35$ は $2\cdot5\cdot3\cdot7$ に精密化される）、この予想は、$\omega$、 $2\omega$、 $\omega^\omega$、さらには $-\omega/7$ のような「完全な」無限小を含む、はるかに豊かな全能整数においても同様の因子の並べ替えが成り立つかどうかを問うものです。

AI駆動型ワークフローの概要

プロジェクトは5週間のフェーズで進行し、各週でエージェント、その役割、およびLeanとの対話を洗練させました。

1. 第1週 – ナイーブなワンショット試行

Claudeに対して予想の「ブレイクスルーを起こせ」とプロンプトを入力。
Claudeは専門用語を多用した長く支離滅裂で検証不可能な文章を生成。
ChatGPTの「懐疑的」なペルソナに切り替えたところ、短くもっともらしい補題は得られたが、一貫した証明には至らず。

2. 第2週 – マルチエージェントラボ

決定論的なトークン使用のためにCodexをローカルにダウンロード。
明確な役割を持つエージェントを生成：PM（プロジェクトマネージャー）、Math（アイデア生成）、Red（敵対的レビュー）、Random（探索）、Lean（形式化）。
エージェントは共有の「カフェテリア」チャンネルで通信し、PMがマージを調整。
このワークフローにより膨大なTeXコーパスが生成されたが、検証済みの新しい結果は得られず。

3. 第3週 – 行き詰まりとトークンの枯渇

Leanの形式化のために再びClaudeを導入。モデルは自身の主張を証明したり、後に否定したりと揺れ動いた。
TeXスタックは約30の「論文」にまで成長したが、一つのミスが塔全体を崩壊させるリスクを孕んでいた。
有望に見える全体的な証明が現れたが、新たな監査により循環参照が露呈し、まだ証明が存在しないことが確認された。

4. 第4週 – 現実への回帰

査読済み文献（L’Innocente–Mantova 2024）の具体的な誤りの検証に焦点をシフト。著者といくつかの誤植を確認し、モデルが現実の問題を見抜く能力に対する信頼を確立。
それまでのコーパスをすべて破棄し、ChatGPTに数学的に健全なものを救い出すよう依頼。
文献の中に有限次数の素数性に関する結果を発見し、検証の結果、それが新規の定理であることが判明。

5. 第5週 – 統合と最終証明

2つ目の独立したLeanエージェントを構築し、新規の結果を証明させる一方、最初のLeanエージェントには確立された文献のみを扱わせた。
厳格なスタンドアロンフォルダ（内部インポートなし）を導入し、追加の公理、モジュールの階層化、証明サイズに対する自動監査を実施。
証明マップ（Mermaid図）を生成して依存関係を可視化し、モデルが不要な枝を剪定できるようにした。
「楽しんで」というプロンプトを繰り返した後、エージェントは追加の公理なしでコンパイルされる、完全な精密化予想のスタンドアロンLean証明書を生成した。

主要な技術的成果物

成果物	説明
GitHub repo – `gaearon/conway-refinement`	Leanソース、TeXドラフト、ツールスクリプトを含む。
Palomar registry entry – `PALOMAR‑2026‑09‑03‑000002`	Leanカーネルが証明を受け入れたことの機械的検証。
Standalone folder	Mathlibのみをインポートするファイル群。各500行以下の人間が読めるステートメント。
Proof map website – `gaearon.github.io/conway-refinement`	証明の依存関係ツリーを示すインタラクティブなMermaid図。
Custom tooling – `subverso` 属性アノテーター、モジュールシステムリンター、Lean Comparator統合	クリーンなモジュール階層を強制し、隠れた公理を防ぐ。

学んだ教訓（結論から）

AIは、著者が数学を理解していなくても、難解な未解決問題の機械的に検証された証明を生成できる。ただし、ワークフローには厳格なエンジニアリングのガードレール、敵対的な監査、頻繁な「破棄して再構築」のサイクルが必要である。
探索的な数学においてはChatGPTの方がClaudeよりも有用であり、具体的な目標が与えられた際の決定論的なLeanコード生成ではClaudeが優れていた。
信頼できる文献と推測的な結果のためにLeanパイプラインを分離することで、汚染を防ぎ、監査を容易にできる。
低レベルの誤り（ソース論文の誤植など）を人間が検証することで、モデルの出力に対する信頼が高まり、コラボレーションの足がかりとなる。
証明マップの可視化と厳格なモジュールの分離は、モデルの解釈可能性を劇的に向上させ、エージェントが「デタラメな」枝を剪定することを可能にする。
トークンコストは莫大であり、全工程で約400億トークン（約4万ドル）を消費した。より良い制御を行えば、これを5〜10分の1に削減できる可能性がある。

代表的なコミュニティの反応

「このプロセスは、著者が数学を全く学んでいないのに、モデルが重労働をこなすパフォーマンスアートプロジェクトのように感じる。」 – m‑steffen, HNコメント

「ChatGPTの懐疑的なペルソナは、Claudeの壮大なワンショット試行よりもはるかに生産的だった。」 – nphardon, HNコメント

「証明マップとMermaid図は、モデルが証明の形状を把握し、簡略化を提案するのに役立った。」 – 著者自身の観察

未解決の課題と次のステップ

独立した数学的レビュー – 証明はまだ超現実数の専門家によって精査されていません。コミュニティによる検証が不可欠です。
簡略化 – 現在のLeanコードには多くの補助的な補題が含まれています。より短く、より概念的な証明があれば受け入れられやすくなるでしょう。
一般化 – このワークフローは他の未解決問題にも適用可能です。テンプレートリポジトリを準備中です。
コスト削減 – より良いプロンプト戦略とトークン効率の高いエージェントを開発することで、大規模なAI駆動型数学をより身近なものにします。

最終的な結論

複数のLLMエージェントを調整し、厳格なLean形式化を強制し、ハルシネーションによる数学を繰り返し剪定することで、Conwayの精密化予想の機械的に検証された証明を生成することに成功しました。この結果は、AIによる定理証明が、著者の専門知識をはるかに超える問題であっても実現可能であることを示していますが、同時に、正確性と信頼性を確保するためには、規律あるエンジニアリング、敵対的な監査、そして人間とのコラボレーションが不可欠であることも浮き彫りにしています。