For something I am planning to write, I need to clarify few issues with respect to computer-aided proofs that we cannot verify every step by hand. For example, the proof for the four-color map theorem.
- Would it be correct to state that given the result of the computer program, if the program itself is correct (can be proven to be correct), and if the other parts (hardware) are known to be functioning as they should be, then the program combined with the output is the proof itself. By that, I mean that not being able to check every step of the computation is something we wish we could have achieved, but nonetheless has nothing to do with the validity of the proof. (All this may seem trivial; my motivation for this post is that not all mathematicians view the result in the same way.)
- Are there other such computer-aided proofs as famous (or so) as four color theorem?
The Kepler conjecture has been proven by computer. Actually, it has also been proven that the proof by computer is true, the wikipedia page behind the link tells the story of the proof and its proof.