四色問題の証明でコンピュータが行ったのは膨大な場合分けのしらみつぶしの部分だよ。

「考える」の定義に依存するけれど、コンピュータができるのは（Prologなんかを用いても）
形式的なパターンマッチングや分岐の追跡が限界です。
証明の方針を与えたり「発想」する部分は今のコンピュータじゃまだできません。