Abstract:
There is a strong analogy between proving theorems in mathematics and writing programs in computer science. This paper is devoted to an analysis, from the
perspective of this analogy, of proof in mathematics. We will argue that while
the Hilbertian notion of proof has few chances to change, future proofs will be of
various types, will play different roles, and their truth will be checked differently.
Programming gives mathematics a new form of understanding. The computer is
the driving force behind these changes.