Proof Assistants and Their Applications in Mathematics and Computer Science

Since their beginnings in the 1960s, proof assistants (also called interactive theorem provers) have grown to become essential tools to establish the correctness of hardware and software and to computerize mathematical theories.
Specifically, proof assistants are computer programs that help users formally describe mathematical statements and proofs, making them amenable to mechanical checking. Today these programs are used to verify microprocessor designs, operating systems, compilers, and cryptographic protocols-as well as landmark results in mathematics such as the odd order theorem in finite group theory and the Kepler conjecture about sphere packing. Contemporary proof assistants rely on a sophisticated interaction between theoretical investigations in metamathematics and the efficient implementation of a portfolio of algorithms. This volume is designed to be an introduction to these fascinating topics.
Topics and features:
- Guides the reader through decades of research into designing and using proof assistants
- Provides convenient, appropriate citations for the proof assistants' underlying logical formalisms, architectures, and applications
- Grounds the exposition by starting with key topics that are treated across all relevant logical foundations and systems, in a system-agnostic and logic-ecumenical way
- Builds on those core topics in the second part, which is dedicated to a gallery of achievements in mathematics and computer science
This unique volume is designed to serve as a useful resource both for early or more established researchers in interactive theorem proving and for researchers in mathematics, computer science, and philosophy-as well as for engineers who want to use proof assistants.
The volume is edited by Jasmin Blanchette, professor at the Ludwig-Maximilians-Universität München, Germany, and Assia Mahboubi, senior researcher at Inria, France, and endowed professor at the Vrije Universiteit Amsterdam, the Netherlands.

Jasmin Blanchette earned his PhD degree in computer science in 2012 from the Technical University of Munich (Germany). He has been active in Germany, France, and the Netherlands, before coming back to Munich. Since 2023, he is professor at the Ludwig-Maximilians-Universität München, where he heads the Chair for Theoretical Computer Science and Theorem Proving. His research focused on using and developing interactive and automatic theorem provers.
After graduating in pure mathematics, Assia Mahboubi earned her PhD degree in computer science in 2006 from the University of Nice Sophia Antipolis (France) and her habilitation degree from Nantes University (France). Since 2017, she has been a researcher at the French research institute Inria, conducting research in dependent type theory and formalized mathematics.