The Computer Science Colloquium

Sergei Artemov
(Graduate Center CUNY)

"Computer-Aided Proofs"

Computer-assisted proofs are playing an increasingly visible role in mathematics, computer science and industry. Proof assistants have reached the stage where they can be used for formalization and certification of real mathematical theorems, such as the Jordan curve theorem, the prime number theorem, the Goedel incompleteness theorem, the four-color problem, and other famous mathematical results. There are a variety of systems now available ranging from model checkers and fully automated provers for propositional logic to sophisticated proof assistants for higher-order theories; the latter provide user-friendly and theoretically well-founded comprehensive tools for creating, handling, and using formal proofs. These techniques have been used successfully in industry for hardware and software verification.

In this talk we will review the history and discuss some questions concerning these developments. To what extent can one trust computer-generated proofs? Are such proofs more trustworthy than conventional hand-checked proofs? Do incompleteness phenomena extend to the foundations of verification? For that matter, can a verifier be verified?

The Colloquium is supported by generous contributions from the Bloomberg, Information Builders, Inc. and Netlogic, Inc.