計算機での自動証明の話で、
ヒルベルトのプログラムだのゲーテル数だのを持ち出す方が
よっぽどバカだと思うのだが．．．。
そういう無茶な風呂敷の広げ方をするから、
一般人は>>500のような反応をするわけで。

実際に自動証明の研究でやっていることはといえば、特定の分野で
限られた定理の組合せで証明できる範囲に限定して、
前提となる事実・帰結・推論規則としての定理・定理を適用する上でのノウハウ
等を、その範囲に限定して設計された記述言語で記述しておいて、
それらを利用して、人間には比較的簡単に行えるような証明を構築するプロセスを
計算機にトレースさせるというような試み。
つまり、人間にできないような証明を計算機にやらせるなんてことを
いきなり目指してるのではなく、まずは人間の思考というものを
プログラムでモデル化してみることで、人間的な有機的な物事の捉え方を
計算機で応用するための知見が得られないかを探る基礎的な研究であって
本質的には人間工学に近い分野。あとはノレッジベースとかＡＩ（死語）とか。

実際に素材としている数学の分野は、簡単な定理の組合せで証明できる
初等幾何が主流。それも、ピタゴラスの定理のように数値の計算が
からむようなものは「簡単な定理」の範囲に入らない。