ケプラー予想や四色問題は証明の本質的な部分に計算機による膨大な計算があったから、
その部分の検証に時間がかかったとうことで、
論証のステップに飛躍ありまくりのIUTとは本質的に異なる
望月のご託宣で議論が進められているIUTの「証明」を形式化するのは不可能だろｗ