個人開発者、Claude を用いて Conway の超現実数に関する 50 年越しの未解決予想を証明
非数学者が Claude と共に一ヶ月間トークンを投じて全オムニフィック整数に対する共通細分予想の Lean 証明を完了させた事例。
リリース: 2026-09-18 · 読了 4 分記事の要約
1. 核心（What）
- 著者が Claude と協働し、John Conway が 1976 年に提唱したオムニフィック整数の共通細分予想に対する Lean 証明を構築したと発表
- 超現実数の定義やこれまでの進展を踏まえ、Claude が対象とする未解決問題として同予想を選定
- TeX 形式に変換した関連論文を LLM に読み込ませ、インタラクティブなセッションを重ねて証明のコードを完成させた
- 作成した証明は Palomar レジストリの機械的検証を通過している
2. 影響（Why）
- 専門知識なき問題解決の可能性: 数学的背景を持たない開発者でも、LLM の自律的な推論と定理証明系を組み合わせることで難解な未解決問題の形式化・証明に到達できる点を示した。
- 国内数理チームへの実証的インパクト: 国内の数理モデル検証を手がける研究組織は、AI を活用した探索的証明構築の有効性と限界を評価するベンチマークとしてこの事例を参照できる。
3. 根拠・詳細（How）
- TeX 変換によるコンテキスト最適化: PDF を都度デコードさせるのではなく、事前に関連論文を TeX 形式へ変換してモデルに読み込ませることで推論コストとトークン効率を最適化した。
- Palomar レジストリによる機械的検証: 構築された証明コードを Lean 形式で記述し、Palomar レジストリの機械的チェックを通すことで論理的な整合性を担保している。
4. 展望・課題（Next）
- 独立した数学的査読の必要性: 現時点では数学者コミュニティによる独立した厳密な査読が未完了であり、Lean カーネルのバグに依存していないかの検証が求められる。