プルーフ・チェッカーはまだいいけど自動証明に期待をもつってのは、
ＡＩの研究者以外では数学の出来ないやつだけだろ。
自分の代わりに機械にやってもらおうと。そんなの何の意味があるか
知らないけど。宿題やってもらうとかかｗ