A Survey of Interactive Theorem Proving

Abstract

Fully formally verified mathematics and software are long-standing aims that became practically realizable with modern computer tools. Reasoning can be reduced to several basic logical principles, and performed using specialized software, with significant automation. Although full automation is not possible, three main paradigms are represented in formal reasoning tools: (i) decision procedures for special classes of problems, (ii) complete, but potentially unterminating proof search, (iii) checking of proof-sketches given by a human user while automatically constructing simpler proof steps. In this paper, we present a survey of the third approach, embodied in modern \emph{interactive theorem provers (ITP)}, also called \emph{proof-assistants}. These tools have been successfully developed for more than 40 years, and the current state-of-the-art tools have reached maturity needed to perform real-world large-scale formalizations of mathematics (e.g., Four-Color Theorem, Prime Number Theorem, and Feith-Thompson's Odd Order theorem) and software correctness (e.g., substantial portions of operating systems and compilers have been verified). We discuss history of ITP, its logical foundations, main features of state-of-the-art systems, and give some details about the most prominent results in the field. We also summarize main results of the researchers from Serbia and personal results of the author.