Comment by riku_iki

> But given a well specified problem, it can bruteforce search through lean tactics space at an extremely superhuman pace. What is lacks in intuition and brilliance, it will make up in being able to explore in parallel.

right, but because math is not well specified and formalized yet, it could be a problem, and that's where humans with intuition and more rigid reasoning still necessary.