AI による数学的証明：全無限整数におけるコニーウェイ予想への挑戦記

数カ月前から AI が数学問題を解くという話題は注目を集めていました。「画期的な成果を達成せよ（Do a breakthrough）」というフレーズはすでにミーム化していました。 数学初心者である私が、未解決問題を探求し、最先端の AI モデルに解いてもらうプロジェクトを開始しました。

このプロジェクトには膨大なトークンと余暇が必要となりましたが、最終的にジョン・コニーウェイ氏が 50 年前に提示した予想（全無限整数の微細化性質）に関する証明を得られたと信じています。

注意: 本証明は現時点で数学者による独立検証はされていませんが、パロマールのレジストリでの機械的チェックを通過しており、専門家からは「妥当に見える」と評価されています。本記事では、そのアプローチと学んだことを紹介します。

---

1 日目：分野の選定と問題の定義

私は数学の本質を理解せずに解決しようとするのは非合理的だと考えました。単なる結果ではなく、私に「引き寄せられるもの」を追求しようとしました。

分野の選定：超実数（Surreal Numbers）

Claude という AI モデルに未解決問題を提示させました。超実数はジョン・コニーウェイ氏による発見・発明の系であり、以下の要素を含む豊かなシステムです。

• 通常のすべての実数: $0, -5, 36.6, \sqrt{2}$ など
• すべての序数: $\omega, \omega+1, \omega^\omega$ など（無限大の概念）
• 奇妙な組み合わせ: $75 + \omega \times 3 + 1/\omega$ など

超実数の生成ルール

このシステムは単一のルールから派生します。 「左側にある全てのもの」と「右側にある全てのもの」の隙間（Gap）に新しい数を発生させるというプロセスを永遠に繰り返すことで構成されます。

1. 1 日目: 「何もない」と「何もない」の間に隙間ができ、0が生まれる。
2. 2 日目: 隙間が増え、-1と1が発生する。
3. 3 日目: 隙間がさらに増え、-2, -1/2, 1/2, 2などが発生する。
4. $\omega$（無限日目）: 実数系全体、および無限大・無限小の数が得られる。

このルールを無限に繰り返すことで、一貫した演算が定義された豊かな系へと発展します。

問題の選定：コニーウェイ予想

Claude は以下の未解決問題を提示しました。

• 問題: 「$K((\mathbb{R}^{\leq 0}))$ 内の無限サポートを持つすべての既約元は素数か？」
• 背景: これはコニーウェイの 1976 年の予想であり、「全無限整数の任意の 2 つの因数分解は共通のリファイナメント（微細化）を持つ」という主張と一致します。
• 意義: この予想はコニーウェイの数の系に関する唯一残されている未解決問題です。今年はその記念すべき『ONAG』刊行から 50 周年でもあります。

---

1 ヶ月間：試行錯誤とワークフローの構築

第 1 週目：一夜漬けと失敗

AI に直ちに応答させるよう指示しましたが、成功しませんでした。

• 問題: AI が自らの仕事を正当化するために「単語のサラダ（意味のない文章）」を生成する傾向がありました。
  • 例: 「C* の 1 次障壁は剛性的ではない……制御カラムは実証的に共鳴の必要性を証明し……」という SF 小説風の記述が返ってきました。
  • 結論: 生成された文章を検証できず、数学的整合性が欠如していました。

第 2 週目：懐疑主義からの再起動

Claude の表現に疲れ、ChatGPT（Sol モデル） に切り替えました。

• 変化点: ChatGPT は「ほとんど無意味だ」と客観的に指摘し、Claude とは対照的に懐疑的で自制心が働きました。
• 手法:
  • ChatGPT で仮説を生成・検証した後、その結果を Claude の出力と批判的に比較しました。
  • 「フォーク（分岐）」を行い、突破したアイデアだけを別のセッションへ統合しました。
  • 人手だけでは持続不可能なため、より堅牢な設定が必要だと悟りました。

第 3 週目：最初の行き詰まりと「すべてを燃やす」

ChatGPT の許容容量を使い果たし、再び Claude に戻りましたが、数学的な乱雑さに戻ってしまいました。

• 問題:
  • AI が「解決済み」と宣言するが、後に欠陥が見つかる循環に陥りました。
  • 非標準な用語が多く、「本当に数学的なのか」不明確でした。
  • ライリーアン（Lean）形式化も停滞しました。
• 決断: 「すべてを燃やす（Burn it all down）」を決意しました。
  • 過去の成果（論文スタック）を全廃し、ゼロから始めました。
  • 既存のブロックの上に新しいものを置くのではなく、基盤となる数学的文献の誤りを徹底的に見直すことに焦点を移しました。

第 4 週目：基礎を見出すとワークフロー的确立

新たなセッションで再挑戦し、有効なアプローチが見えてきました。

• 役割分担:
  • PM (プロジェクトマネージャー): コニーウェイ予想という目標へ統合する。
  • Lean エージェント A: 既存論文の認定（形式化）に専念する。
  • Lean エージェント B: 新結果の認定に専念する。
  • 数学エージェント: 新アイデアを探索し、Lean エージェントへToDoリストとして渡す。
  • レッド（批判）エージェント: 証明や推論を検証しようとする。
• 成果:
  • 依存するピアレビュー済み参考文献の誤りを発見・修正しました。
  • **「有限度素性」**という新しい結果を Lean で認定し、人間の数学者とも確認しました。

第 5 週目：監査の強化と証明への道

現在の結果だけでなく、将来的な証明に対する信頼性を高めるためにインフラを構築しました。

• スタンドアロンフォルダ: Mathlib（コミュニティ標準ライブラリ）以外は一切コードを使わず、完全な自己完結型ステートメントを目指しました。
• 監査タスク: 追加公理の有無、インポートの規則違反、証明ペアの存在を確認します。
• 命名の整理: 非標準な用語や AI が発明した造語を排除し、アルファベット（A, B, C...）で再命名しました。

円を描いているか？

モデルは毎回試みましたが失敗していました。「私たちは円を描いているのか？」と問いかけると、AI は以下の認識に達しました。

• 現状: 「最後の占有クラス」の問題が残っている。
• 対策: 官僚主義（サブエージェントの多用）を削減し、一人だけでコニーウェイの削減に専念させるルールを実装。
• 結果: 15 分後には暫定的な証明戦略が提案されました。12 時間後には定理が得られ、元のコニーウェイ予想への道が開けました。

---

成果：証明の簡素化と検証

最終的に得られた証明を簡素化し、検証可能な形にしました。

• ツール開発:

  subverso

  というカスタムツールを作り、Lean ソース内の定理を特別属性で注釈付けできるようになりました。
  • これにより、証明構造の Mermaid 図を自動生成できます。
  • ChatGPT が「数学的背骨（必要なノード）」と「不要なノード」を識別するのを支援しました。
• 可視化: 依存ツリーを探索できるインタラクティブ証明マップを作成し、Zulip で公開しました。

---

学んだこと：プロセスから得た教訓

ワークフローの最適解

成功したプロセスは以下の要素を持っていました。

1. 明確な目標: 前方への具体的なゴール。
2. 暫定的な方向: 大まかな方針の確立。
3. Lean による検証: 数時間でギャップを閉じる厳格なチェック。
4. 役割分離: 未熟な抽象化（誤り）と認定済み数学を混同させないため、役割を意図的に分けた。

重要ポイント：用語法と命名

• 用語は不可欠: 数学者とのコミュニケーションだけでなく、内部ドリフトの検出のためにも命名規則は重要です。
• 初期の後悔: 参照された論文に現れる用語のみを使用するように指示しなかったのが間違いでした。早期のスロープ（スリップ）の原因は、AI が独自のアドホック語彙を発明したことにあります。

コストと時間

• トークン消費: 合計約400 億トークン。そのうち出力トークンは約 2.1 億。95% 以上がキャッシュリードでした。
• コスト: API 価格換算で約40,000 ドル。余暇時間も投入しています。
  • より良いグライドと洞察があれば、5〜10 倍安価で行える可能性があります。

「本当に AI だけで可能か？」への答え

• 結論: **「はい、いいえ、そしてまたはい」**です。
  • はい: 数学的理解が浅くても証明を引き抜くことは可能です（「何も知らない」状態でも）。
  • いいえ: モデルは繰り返しドリフトし、工学作業の構造化に失敗することがあります。
  • そしてまたはい: 適切なプロジェクト管理や刺激を与えられた専門的なエージェントによって代替可能です。

---

結論：アマチュア数学者への未来

低く懸垂する果実を取ってしまえば、「何を知らないかの専門家（アンダートーン）」というニッチは狭まります。しかし、未開拓の領域が常に生まれます。

現在はまだ人間研究と AI との調和が完全ではありませんが、時間の経過とともにこれらのツールを使いこなす道が見出されることを願っています。そして、もしかしたら再び**「アマチュア数学者」**としての余地が生まれようかもしれません。

もし証明に欠陥を発見された場合は、Issue を作成するか Zulip でご連絡ください。この成果は多くの既存の参考文献（S. L'Innocente と V. Mantova 氏ら）に感謝して初めて得られました。