# About proofs that we cannot verify every step by hand

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.

1. 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.)
2. Are there other such computer-aided proofs as famous (or so) as four color theorem?
• There are many computer-based proofs these days. Such as the fact that you need at least 17 filled-in squares for a sudoku to be uniquely solvable (they checked basically all 16-puzzles by computer), and that a Rubik's cube is always solvable in 20 moves or less (they checked basically every cube position by computer). The 4-colour theorem is as famous as it is because it was the first computer proof that was too large for a human to ever hope to check it. – Arthur Sep 4 '18 at 9:17
• The proof is in principle a sequence of elementary steps that can each be justified in the axiomatic system. It is the output of the program. But if one can prove the program correct, the program alone should be enough. Peer review (possibly computer assisted) is still required. – Yves Daoust Sep 4 '18 at 9:41

## 1 Answer

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.