ところで定理を証明するプログラムはすでに存在する
だからそういう意味では人工知能は原理的には可能である

ただこのプログラムは定理でないものを証明しようとすると
延々と動いたまま止まらなくなる　
そういう意味では「アルゴリズム」ではない
（もっともこのことはいうほど問題ではない
　数学者だってそんなことをいったらアルゴリズムではないから）