Comment by cubefox

> We'll automate mathematics because we can, because it's useful.

No, it's not useful. Proving the Riemann hypothesis has no practical application whatsoever. Neither has any of the thousand Erdős problems. Or the Goldbach conjecture. Or the Collatz conjecture. Etc.