>>19
それはLEANカーネル(つまりソフトウェアとしてのLEANコンパイラの心臓部分)にあった不具合だね
もう治ってる
たぶん勘違いしてるけどLEANはオープンソースで誰でも自分のPCでLEAN環境を構築出来るよ
世界中の色んなハードで試されてるからLEAN以外の欠陥の可能性は心配しなくて良い
今かつてないほどLEANが注目されてるので、さすがにもうこれ以上バグ(抜け道)は無いんじゃないかな
もし仮にLEANの不具合がさらに見つかったら、それを修正した上でかつての証明たちが修正後も正しいことを機械的に確認すれば大丈夫
【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]
44名無しのひみつ
2026/09/13(日) 11:55:06.36ID:cZ4BtS3fレスを投稿する