最重要★★★★★Anthropic
Claude、11日でフェルマー最終定理をLean検証
30秒で把握
- 1Claudeが11日でフェルマー最終定理の完全なLean証明を構築
- 21,300万行のコードで30,300定理を検証し最終証明に29,500を利用
- 3Prove2Me上の数十エージェント協調で数学証明の形式化を実行
要約
Anthropicは、Claudeが11日間でフェルマーの最終定理（FLT）の完全なコンピューター検証済み証明をLeanで構築したと発表した。Claudeは約1,300万行のLeanコードを書き、30,300定理を検証し、最終証明では29,500定理を利用した。数十のClaudeエージェントが協調し、Prove2Me上でWilesの証明を簡略化した構成に形式化した。完成した証明はLeanの標準公理3つだけを使い、Leanが検証した。今回の新規性は定理の発見ではなく、人間なら年単位の確認を要し得る複雑な証明を機械的に検証可能にした点にある。
あなたへの影響
AI・数学研究に関わる日本のエンジニアは、LeanとMathlibを使った形式化ワークフローを小規模な定理で検証し、AI生成結果を人手だけで承認しない運用を始めるべきです。
推奨：形式化証明は、人間向けの説明を置き換えずに、論理の各段階をproof assistantで検査する成果物です。