Suppose there was a machine that was a black box where you could ask it whether a result was true or false, and it spit out a truth certificate that was not humanly understandable, but it could be mechanically verified.
I would find this incredibly disappointing. The appeal of mathematics is not just that I know things are true -- I know why they're true. I know why x + y = y + x, why there are infinitely many primes, why the derivative of x^2 is 2*x. Working out a proof isn't tedium -- it's the point.
I would find this incredibly disappointing. The appeal of mathematics is not just that I know things are true -- I know why they're true. I know why x + y = y + x, why there are infinitely many primes, why the derivative of x^2 is 2*x. Working out a proof isn't tedium -- it's the point.