>>110
lean が「正しい証明」と承認した証明に文句を言う数学者は一人もいない
そしてそれが何を証明したかなど誰でもわかる
よって望月論文をleanに翻訳する際に何がどうなっても最終的にABC予想が証明されたのならそれを否定する人間はいない
lean に入力されたコードがiutそのものかなどどうでもいい