4 ms·

To me, that feels more like a limit on human cognition than a fundamental quality of the proof or the program. After all, you can summarize--or, perhaps compres

by tikhonj 13y ago

To me, that feels more like a limit on human cognition than a fundamental quality of the proof or the program. After all, you can summarize--or, perhaps compress--the proof into a program which checks the cases. It's simply a level removed from how mathematicians normally work. On the other hand, if a proof could not be reduced at all--and, given my very limited understanding of information theory, this is possible--then I would certainly agree that it's inherently more complex. Put another way, I think that using a computer to check cases like this is morally similar to using induction. It still exposes and exploits a certain simplicity in the domain.

lmm 13y ago
There was no induction; the proof was essentially: a) all planar graphs can be reduced to these several hundred cases (this part is ordinary mathematics) b) observe that it's possible to four-colour each of these several hundred cases (and a computer program was used to verify it). To my mind the proof is as complex as that set of cases; the fact that we can write a relatively simple program to check them all doesn't really reduce the complexity or tell us anything about why they're all 4-colourable, in the same way that using a computer to check the riemann hypothesis up to some limit tells us nothing about why it holds.
- tikhonj 13y ago
  I know it was not induction. My point is that a computer program to consider all the cases is just another mathematical tool morally similar to induction. The program does tell us something, namely that the problem can be reduced to a bunch of similar cases all of which are colorable. The difference is that the insight is perhaps a level removed from a normal proof. Essentially, I think that it's the program and not its output that plays the philosophical role of the proof in this case. Of course, my perception is significantly colored by the fact that I'm mainly interested in programming languages rather than traditional math :P.

by tikhonj 13y ago

lmm 13y ago

There was no induction; the proof was essentially: a) all planar graphs can be reduced to these several hundred cases (this part is ordinary mathematics) b) observe that it's possible to four-colour each of these several hundred cases (and a computer program was used to verify it). To my mind the proof is as complex as that set of cases; the fact that we can write a relatively simple program to check them all doesn't really reduce the complexity or tell us anything about why they're all 4-colourable, in the same way that using a computer to check the riemann hypothesis up to some limit tells us nothing about why it holds.

tikhonj 13y ago
I know it was not induction. My point is that a computer program to consider all the cases is just another mathematical tool morally similar to induction. The program does tell us something, namely that the problem can be reduced to a bunch of similar cases all of which are colorable. The difference is that the insight is perhaps a level removed from a normal proof. Essentially, I think that it's the program and not its output that plays the philosophical role of the proof in this case. Of course, my perception is significantly colored by the fact that I'm mainly interested in programming languages rather than traditional math :P.