22/11/23 15:11:49.25 fDR3NyfP.net
結局絶対的な正しさは証明検証ソフトであろうと人間査読者であろうと
保証されないのだ。
査読者が証明を精査して、これは正しいといったとしても、その査読者
が（本当は理解せずに）正しいと行っているだけかもしれないし、
あるいは頭が狂っているだけかもしれない。
多数の頭で検証すれば良いと考えるかもしれないが、判断が割れたら
多数決で決まるみたいなことでいいのだろうか？
また、能力差というものがある。たとえば人間が初等幾何の簡単な定理
を証明したとしても、それをチンパンジー並の知性、猫の知性では
とうてい理解できないように、人類を遙かにしのぐ知性の宇宙人の文明
から送られてきた定理や証明などは、人智を遙かに超えていて、まったく
理解もできないか、定理を理解できても証明をフォローして理解できる
レベルに人間の脳神経系は到達していないかもしれない。宇宙人から
みれば、地球人の知性は、地球上で人間が鶏をみるときの知性程度かも
しれないのだから。宇宙人の話ではなくとも、未来のコンピュータは
人智を越えたレベルの能力を持ち、人間では到底証明できないような
複雑で長大な証明をこなすようになっているかもしれない。しかし
それが本当に絶対に正しいのかは誰にも検証ができないかもしれない。
現代のマイクロプロセッサ（CPU)に回路上のバグが無いことや、
OSのコードやコンパイラや計算ソフトにバグが無いことを保証し難い
ように、結局のところ大体正しい、その正しさの程度の相対的な問題
であるのが現実だと思う。100年間正しいと思われていた数学の定理
でも、証明にバグが無いとは云えないだろう。その例の一部は
選択公理等を暗黙に仮定して証明がされていた時代が長くあった
ことなどがある。