ヒルベルトの幾何学基礎論の、ピタゴラスの定理の証明は
原理的に計算機でチェックできるくらい厳密じゃないのかな
（実数論の公理を一寸手直しする必要があるかもしれない）

もっとも、この本は全く直観を排して書かれていることで有名だけども、
それでもとある「明らかだが証明が難しい」定理が、
"困難も無く"得られることになっているのだがｗ