注目★★★★★Hacker News
AIとLeanでConway予想の証明に挑戦、未検証の成果
30秒で把握
- 1著者がAIとLeanでConway精緻化予想の証明を作成
- 2Palomar registryの機械検査を通過、数学者の独立検証は未実施
- 3Claude・ChatGPT・Codexで生成と反証を反復、循環論法も発見
要約
著者はAIエージェントとLeanを使い、50年前にJohn Conwayが提起した精緻化予想の証明を得たと主張した。予想は、omnific integerの積 ab = cd に対し、共通の因子分解を構成できるという内容だ。証明はPalomar registryの機械的チェックを通過し、Leanと対象分野に詳しい複数人も命題の妥当性を認めたが、数学者による独立検証は未実施である。試行ではClaude、ChatGPT、Codexのエージェントに数学・反証・Lean形式化などの役割を割り当て、生成物の循環論法や誤りを何度も発見した。著者は、AIだけで数学的成果を得られる可能性を認めつつ、最終的な信頼性には人間による検証が必要だとした。
あなたへの影響
AIで生成した数学証明を扱う研究者や開発者は、Leanのカーネル検査だけで結論を確定せず、独立した数学者によるレビューと参照文献との照合を組み込むべきです。
推奨：形式化は命題や推論の検査に有効ですが、前提の取り違えや循環論法までは自動的に防げない可能性があります。