Different kind of proofs.

Question

In mathematics the four color theorem have been proved by letting a computer checking each case, thus proving that each map can be colored by only four colors.

However, this made me think about the underlying nature of proofs in general. Suppose we want to prove a statement and we find a proof, but only by letting a computer run an algorithm and checking each case seperately. Now are we really satisfied with this? The proof has given us no understanding at all for why the statement is true, only that it is true.

So we want to find another proof which is more explanatory and can be constructed in a logical way by a human. But is it true that such a proof exists? Can we prove that such a proof exists or that it doesn't exist?

So my final point is: Is there a way to prove that a statement can be proved only using an algorithm or that is can only be proved in a logical way. Or maybe it can be proved both ways or neither way. And really, what is the fundamental difference between theses two?

Answer 1

Current computer algorithms are all Turing-compatible, and that means that at least in theory any machine-proof can be transformed into a 'human-consumable' proof, by which I mean one expressed in the language of first-order logic.

I say 'human-consumable' because if the computer-proof is sufficiently long and complicated, the resulting transformed proof can quickly become a crazy long proof with crazy long and complicated expressions, which means that not only may we just not have enough time to go through the whole thing, but we will very easily lose track of the proof in terms of its organization.

Indeed, we might well end up being merely able to verify that each step does indeed follow some logical inference rule and not much more, and that would certainly not be acceptable for our intuitive notion of a proof, where we demand that we gain some 'clarity' and 'understanding' from the proof, i.e. that it demonstrates to us that is something is so.

Answer 2

To add to what Bram28 said, every practical formal system (including ZFC) can be captured by a program, and arguably there is little difference between the proof of the four-colour theorem by computer assistance in checking cases, and the proof of Kepler's conjecture by hand in the past, which was so long and complicated that people were quite convinced but never completely sure. People are in fact now much more convinced after it has been recently verified by a computer assisted proof!

To answer your underlying questions, I believe some statements are simply true for no particular deep reason. For a simple example the exact values of the Busy Beaver function are simply what they are and there is not going to be any reason for them! Of course, one might hope that certain theorems or conjectures turn out to have deep underlying mathematics, but it is often hard to tell.