8分
フェルマーの最終定理が Lean で機械検証を通った——確かめる側に回るには、153GB のメモリが要る
Claude が 11 日でフェルマーの最終定理の証明を Lean で形式化し、機械検証を通した。依存する公理は 3 つだけ、未証明の穴もなし——ただし自分で全部を再現するには、ピーク 153GB のメモリが要る。
INDEX · KEYWORD
Lean
「Lean」に関連する公開記事をまとめています。
- KEYWORD
- Lean
- 範囲
- 公開記事
- 公開数
- 2本公開
関連記事
2–2 / 全2本
4分
Claudeが証明したのはリーマン予想ではない——「零点の67.2%」という下限と、手元で検証できるLeanのコード
未公開の研究版Claudeが、ゼータ関数の零点のうち臨界線上にあると証明できる割合の下限を41.6%から67.2%へ引き上げた。リーマン予想は解けていない。注目したいのは記録より、その証明がLeanで形式化され、誰でも手元で通せる形で公開されたことのほうだ。