4 ms·
A reason to dislike computer-generated proofs: The point of mathematics is not just to know whether some proposition is true, it's to understand the mathematic
by DavidSJ 10y ago
A reason to dislike computer-generated proofs:
The point of mathematics is not just to know whether some proposition is true, it's to understand the mathematical objects under study. A beautiful proof sheds light, it explains why.
- bonobo3000 10y agoyeah. adding to this, a great proof that uses new techniques can also generate whole new areas of math to explore or solve other seemingly unrelated problems.
- jonnybgood 10y agoTo use a famous example: The proof of Fermat's last theorem.
- Kenji 10y agoThat's your view on the point of math. I would be perfectly content to have a long, computer generated proof of P ?= NP. Of course I prefer beauty and elegance in proofs, but I think leveraging the computer as a tool to prove things for us is quite an elegant thing by itself.
- dredmorbius 10y agoLook up the concepts of "mathematical beauty" or "mathematical elegance". This isn't an idiosyncratic preference of GP.
- pron 10y agoI think P vs. NP is one proof where insight matters a lot. As Scott Aaronson said, if CS were physics, we would have declared P != NP a law of nature a long time ago. We basically know it to be true already. A proof that we can't understand adds almost no information in this case.
- Scarblac 10y agoIt would be horrible if we had an impossible to understand, but correct, proof of P = NP that gave no hint of how to actually construct polynomial algorithms for those problems.
- curryhoward 10y agoInterestingly, there are algorithms for solving NP-complete problems which are provably polynomial time iff P = NP. So the moment P = NP is proven, we immediately know of polynomial-time algorithms for NP-complete problems. We have the algorithms today, we just don't know if they are in P. https://en.wikipedia.org/wiki/P_versus_NP_problem#Polynomial-time_algorithms https://en.wikipedia.org/wiki/P_versus_NP_problem#Polynomial...
- Scarblac 10y agoHuh, thanks! That's completely surprising to me. Edit: ah ok, a semi-algorithm that just tries all possible programs...