In a complete formal proof of a theorem, each step follows from the previous steps using formal deduction rules. Ideally, such a process is so systematic that it could be checked mechanically by a program.

Since proofs are supposed to be mechanically checkable, we may think of using a computer to produce proofs of true theorems automatically. Russel and Whitehead, in Principia Mathematica, tried to write down a sufficient set of axioms that would let us prove everything interesting. Then Hilbert posed (as one is his 23 famous problems) the problem of finding such a method. One of the great accomplishments of 20th century mathematics is the proof that no such method exists. In fact, we do ...

Get Discrete Mathematics now with the O’Reilly learning platform.

O’Reilly members experience live online training, plus books, videos, and digital content from nearly 200 publishers.