3 ms·

It should be noted that there is some reason to aesthetically dislike computer-generated proofs. It's not mentioned by Baez, but one of the first breakthroughs

It should be noted that there is some reason to aesthetically dislike computer-generated proofs. It's not mentioned by Baez, but one of the first breakthroughs in the Erdos discrepancy problem was a very verbose (running into a few GBs if I remember right), computer generated proof, for a subcase. Terry Tao later presented a general proof which was far far shorter. Obviously there are cases like the 4-color theorem which have withstood the test of time and prejudice, but there is something sad about not being able to make sense of such math.

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 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 ago
    yeah. 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 ago
      To use a famous example: The proof of Fermat's last theorem.
  - Kenji 10y ago
    That'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 ago
      Look up the concepts of "mathematical beauty" or "mathematical elegance". This isn't an idiosyncratic preference of GP.
    - pron 10y ago
      I 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 ago
      It 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 ago
        Interestingly, 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 ago
        Huh, thanks! That's completely surprising to me. Edit: ah ok, a semi-algorithm that just tries all possible programs...
- jonnybgood 10y ago
  In what kind of situation would a proof need to be reproduced?
  - drauh 10y ago
    Sorry, I meant "verified". I was thinking along the lines of science.
- ittekimasu 10y ago
  For 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.
Retra 10y ago
It should also be noted that with a finite vocabulary, the vast majority of interesting mathematical theorems cannot be stated in a reasonable amount of time.
- benkuykendall 10y ago
  I'm having trouble understanding this statement and its motivation. Under what definition of "interesting" can any "unreasonably" long theorem statement be of interest to humans, and what makes you this class of theorems is numerous?
  - adrianN 10y ago
    Thm: There are no uninteresting theorems. Proof: Assume there are uninteresting theorems. Let T be the shortest such theorem (under some fixed encoding). Having the special property of being the shortest uninteresting theorem makes T interesting. qed.

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 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 ago
  yeah. 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 ago
    To use a famous example: The proof of Fermat's last theorem.
- Kenji 10y ago
  That'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 ago
    Look up the concepts of "mathematical beauty" or "mathematical elegance". This isn't an idiosyncratic preference of GP.
  - pron 10y ago
    I 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 ago
    It 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 ago
      Interestingly, 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 ago
        Huh, thanks! That's completely surprising to me. Edit: ah ok, a semi-algorithm that just tries all possible programs...
jonnybgood 10y ago
In what kind of situation would a proof need to be reproduced?
- drauh 10y ago
  Sorry, I meant "verified". I was thinking along the lines of science.
ittekimasu 10y ago
For 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.

Retra 10y ago

It should also be noted that with a finite vocabulary, the vast majority of interesting mathematical theorems cannot be stated in a reasonable amount of time.

benkuykendall 10y ago
I'm having trouble understanding this statement and its motivation. Under what definition of "interesting" can any "unreasonably" long theorem statement be of interest to humans, and what makes you this class of theorems is numerous?
- adrianN 10y ago
  Thm: There are no uninteresting theorems. Proof: Assume there are uninteresting theorems. Let T be the shortest such theorem (under some fixed encoding). Having the special property of being the shortest uninteresting theorem makes T interesting. qed.