>>7
4色定理が有名だけど、
単純な機械的探索ではなく、
上手く解を見つけるためのチューニングを施している。
しかも、証明の土台は過去の先人が築いたもので、
場合分けが多すぎるのをコンピュータでカバーしただけだしな。

将来的にコンピュータが人間並みに定理を証明するような時代が来ないとは言い切れないが、
今のAI技術からするとまだまだ幾つものブレークスルーが必要。