Logic seminar

Interactive theorem proving for the working logician

Over the last few decades, computational proof assistants have made it possible to construct formal axiomatic derivations of increasing complexity. They are now used to verify that hardware and software designs meet their specifications, as well as to verify the correctness of mathematical proofs. The practice has taken root and promises to play an important role in mathematics and computer science.

In this talk, I will survey the technology, with an emphasis on formal mathematics. I will then discuss aspects of interactive theorem proving that may be of interest to the working logician, and places where a better theoretical understanding can lead to progress. Specifically, I'll discuss the need for practical foundations, search procedures, decision procedures, and proof systems.