コナウィの予想の証明を感じ取った
概要
- 数ヶ月前、AIによる数学の進展が話題となり、自分も未解決問題にAIで挑戦
- John Conwayの50年前の精緻化予想（refinement conjecture）の証明に挑戦
- Leanによる機械的検証はクリア、ただし独立した数学者による検証は未実施
- 問題選定からAIとのやりとり、失敗と試行錯誤の過程を詳細に記述
- Surreal numbersやOmnific integersの基礎説明も含む
AIとConway精緻化予想への挑戦
- AIによる数学的ブレークスルーが注目される中、自分も未解決問題にAIで挑戦した経緯
- John Conwayが提唱した 精緻化予想 （refinement conjecture）への関心
- omnific integers に関する予想内容：ab = cd ならば、それぞれa, b, c, dを組み替えられる整数e, f, g, hが存在
- Leanによる証明を得るまでに 1ヶ月 と大量のトークンを消費
- Palomar registryの 機械的チェック は通過、Leanや分野に詳しい数名からも「正しそう」と評価
Surreal Numbers（超現実数）の基礎
- Surreal numbersは John Conway による新しい数体系
- 全ての実数 ・ 全ての順序数（ordinal） ・それらの組み合わせを内包
- 一つのルールから無限に数を生成する 再帰的構築法
- 例：初日に0、次に-1と1、さらに-2, -1/2, 1/2, 2…と生成
- 無限回繰り返すことで、実数・順序数・無限大・無限小まで含む体系が誕生
問題選定とAIへの依頼
- Claudeに「Surreal numbers分野で未解決の魅力的な問題を選んで」と依頼
- Claudeが選んだのが Conwayの精緻化予想
- K((ℝ^≤0))における無限サポートの既約元が素元か？という問題と同値
- ONAG出版50周年の記念もあり、選定理由に共感
- Leanで定式化できるかを確認し、プロジェクト開始を決断
精緻化予想の内容
- omnific integers ：超現実数の中で「整数部分」に相当
- 例：通常の整数3, -5だけでなく、ω, 2ω, ω*ω, ω^ω, -ω/7など
- 予想の主旨：ab = cd ならば、a, b, c, dを分解・組み替え可能
- 通常の整数なら素因数分解の再構成で自明
- 無限や超現実数でもこの「良い性質」が成り立つかが問題
AIとの試行錯誤
- Claudeに「反例探索」や「ブレークスルーを起こせ」と依頼
- Claudeの出力は 用語の創作・根拠なき主張・ドラマチックな文体 で信頼性に疑問
- ChatGPT（Sol）に切り替え、Claudeの出力を批判的に評価させる
- ChatGPTは「ほとんどがでたらめ」と指摘、慎重かつ懐疑的な姿勢が好印象
- 以降はChatGPTを中心に進行、批判的な人格を維持しつつ証明にトライ
結果と今後
- 得られたLean証明は 独立検証待ち だが、AIの支援で未解決問題に実質的進展
- 機械的検証や分野の専門家による初期評価は「正しそう」
- 今後は 数学者による独立検証・反証の呼びかけ を継続
参考リンク
体験から得た教訓
- AIは「言葉巧みに見せかける」出力に注意が必要
- 懐疑的なAI人格との対話が より実用的な進展 を生む
- 未解決問題でも Leanなどの形式的手法 で検証可能性が高まる
- AIと数学の協働は 人間の批判的思考と組み合わせてこそ有効
Surreal numbersや精緻化予想の詳細な数理的解説や、Leanによる証明の技術的経緯はGitHubリポジトリを参照