4 ms·
"… some reason …" Name one? I think I understand that it's unsatisfying that there are instances where mathematics cannot be done with just pencil and paper. H
by drauh 10y ago
"… some reason …"
Name one? I think I understand that it's unsatisfying that there are instances where mathematics cannot be done with just pencil and paper. However, it's a reproducible proof. And folks in science have long gotten over the fact that there are important results that can only be achieved with lots of computing power, and not just pencil and paper.
- DavidSJ 10y agoA 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...
- jonnybgood 10y agoIn what kind of situation would a proof need to be reproduced?
- drauh 10y agoSorry, I meant "verified". I was thinking along the lines of science.
- ittekimasu 10y agoFor one thing, the point of a proof is not its use merely for showing the validity or invalidity of a statement, but in the generation of new approaches/theories. Atleast that's my view of Math; this is not to say either that being able to verify proofs is bad (this is orthogonal), nor is to say that there aren't proofs that can't be worked out by pencil-paper. On a meta level, it seems unlikely that a computer will be able to create theories and abstractions while trying to solve such problem, given the current state of AI, in the conceivable future. I do believe such "unsupervised learning" is necessary for doing math. This of course is quite a different line of work than in PL/Verification where one only cares if something they've written can be proved to satisfy some properties. However, I've heard often that a proof of a program is often as long as the program itself; this is often reflected in the difficulty people have in parsing code without adequate high-level milestones.
- ktRolster 10y ago>Name one? For one thing, there can be subtle errors in a computer proof (overflow is obvious, but compiler bugs, CPU bugs, and RAM errors are not). If you can create a brief proof, then you can avoid all those problems.