Anthropic が示した、Fermat の最終定理を機械に通すという発想
Anthropic が公開したのは、Fermat の最終定理について「新しい数学の発見」ではなく、「既にある証明を Lean で最後まで機械検証できる形に落とし込んだ」成果だ。しかもその作業は、人間が細かく手を動かして積み上げたというより、Claude が 11 日間かなり自律的に進めたものだという。数学の世界では、証明が正しいかどうかを読む人間が何週間も何か月もかけて確かめることがある。そこに AI と proof assistant の組み合わせがどこまで食い込めるのか、Anthropic はかなり強い実演を見せた格好だと思う。 Anthropic の発表によると、Claude は Fermat の最終定理の proof を Lean という programming language に書き直し、computer-checked な形で最後まで通した。Fermat の最終定理とは、正の整数 a, b, c について aⁿ + bⁿ = cⁿ を満たす解は n > 2 では存在しない、という有名な命題だ。17世紀に Pierre de Fermat が書き残したもので、長く未解決だっ
papoo.work