>チェックできない定理の例としては”4色問題”をあげます。もっとも現在プログラムの
>改良が進められたそうで､調べてみないとなんともいえませんが。

幾何学の先生では、「四色問題」が証明されたとは認めていない人もいる。
「四色問題」は、広く定理としては認められていない。

＞＞philosophically weakで何がmathematically uglyなのかな、と思って聞いてみた
＞タルスキーは直観主義について上の言葉で論評したとき例をあげたのですか？

タルスキーに訊けよ。

＞この方法を抽出して計算機のプログラムとすることはできます

そのプログラムが信用できるという根拠は？
誰がバク取りするのかな？
３００年かけて、あなたがバグ取りしてみてはいかが？
そもそも証明論に適用できるようなヒューリスティックな
プログラムなんて、実際に作られたのかな？
実例を挙げてみてください。