>>269はそんな定理があるなんて言ってないだろ
単に、必要があれば、充分形式的なレベルまで証明を緻密にする
自信がある、というだけだろ

証明の形式化のどの部分がそんなに難しいと考えてるのかな？
少なくともZFCの公理から、必要な諸概念を定義して、
完全に形式的に証明するのは、述語論理の基礎を理解している数学者には
簡単なことだと思うがな
今回14年掛かったことだって、単に能力が欠けていた、としか思われない