>>489
> ＞ 証明の方針を与えたり「発想」する部分は今のコンピュータじゃまだできません。
> 体系が単純で簡単な証明なら総当り式でできるでしょう。

「これを証明するには総当たりでいける」と読むところができないのです。