Jordan曲線定理が、ごくごく常識的な公理系から
証明できる、というのは大昔に数学者が確認したことなんだよ
今回の「完全証明」とやらの意義は、Jordan曲線定理を証明するのに
必要な公理の強さを確定したとか言うことじゃなくて、
proof checkerが、実用化に近づいた、ということだろ