証明の中に人類がまだ十分にその存在を意識していない
公理を暗黙に導入している可能性があるからな。
その公理がなければ証明不可能な命題だとすれば、。。。
そういう可能性もある。
証明チェッカーはそういう証明の穴が無いことを
示しうる。
しかし数学的に証明が可能な問題であっても、
それを具体的に書き下すことが事実上不可能な
問題はいくらでもある。たとえば将棋は千日手
を禁止すれば、先手必勝か先手必敗か引き分けか
に必ずなるはずだが、たとえば先手必勝である
というのが真実だとして、それを具体的に証明を
記述してみることは、おそらく誰にもできない。
証明が数学的に可能だとしても、その記述量は
現実的なものではないだろうからだ。宇宙の
すべての原子に0と1を割り当てて記述したと
しても、書き切れない程のビット長の記述文章
になるだろうから。