Thread: 4 color theorem

Once upon a time I read that the 4 color theorem had been proven, but required a computer to prove it for about 2000 cases.

I'm looking for opinions or fact: Is a theorem proved by simply reducing it to cases of such a large number of examples?

some theorems CAN be proved that way. combinatorial problems are particularly amenable to such an approach.

in general, however, merely proving something is true for even a large number of cases does not prove it. a good example is the riemann hypothesis which is known to be true for a LOT of cases, but the general conjecture remains unproven.

there is a notion in some fields of "asymptotic" proof, that is: that the "possible exceptions" to a theorem get farther and farther apart. so, for example, we can calculate a "rough estimate" of the probability whether or not a certain number is prime, without knowing if, in fact, it IS prime. this can be useful.

with regard to computer-aided proofs, usually what is proven is "a proof of the proof": that is, that the algorithm for the program that carries out the proof is correctly written. this in and of itself can be a daunting task (and the devil is in the details). the fact is that computers can carry out calculations that would be unfeasible for mere mortals, especially when large numbers are involved.

The "hard part" is reducing from an infinite number of cases to a finite number. With only a finite number, we can just check every case- even if "finite" is so large you need a computer to check the cases.

Originally Posted by HallsofIvy

The "hard part" is reducing from an infinite number of cases to a finite number. With only a finite number, we can just check every case- even if "finite" is so large you need a computer to check the cases.

Wiles' proof of Fermat's Last Theorem comes to mind here...

For more on the formally verified proof of the four-color theorem, see this issue of the Notices of the AMS.

Just bumping this over the spam