【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]

リーマンはよ

1つでも本当は偽である命題を正しいとすることがこっそりできれば、
それを用いて全ての数学命題についてそれを正しいとする証明ができる。
1千万行のLEANに食わせるソースコードに、間違っているがLEANがPASS
させる命題を作れれば、それを利用してなんでも証明が成功できるだろう。
一種のせキュリティホールだ。
蟻の穴から堤も崩れる（韓非子）