>>108
>Leanがただしいと結論づけてそれを否定する数学者はいない
どうでしょうねぇ
まあそうだとしても
入れたプログラムが正しいと結論したとして
その入れたプログラムがIUTの正しい形式的な翻訳になっているかどうかの確認が必要なのでは？