最近のコンピュータ将棋って結構強いよね。
ルールや対局データを与え、アマチュアには勝てるようにプログラムされている。
自動証明も同じようにできそうだけど、案外自動証明を研究されている方がプログラミングが不得意なのかもしれないよ。
私の従兄弟は数学のセンスは凄いのだけど、プログラムはてんで組めないんだよね。