Proof assistants are computer programs that help users formally describe mathematical statements and proofs, making them amenable to mechanical checking. Today they are used to verify operating systems, compilers, and cryptographic protocols, as well as landmark results in mathematics such as the Feit-Thompson theorem or the Kepler conjecture. Contemporary proof assistants rely on a sophisticated interaction between theoretical investigations in metamathematics and the efficient implementation of a portfolio of algorithms, without which these systems would not usable on a large scale. During the last decade, the use of proof assistants has grown steadily, and they are now at the same time a research topic in its own right and a tool for researchers in other domains. Yet no reference book is available today that covers the entire domain. This book is an introduction and reference for the various topics related to the underlying logical formalisms, architectures, and applications. The main audience is graduate students entering the field of interactive theorem proving, the secondary audience is more established researchers in computer science, mathematics, and philosophy, as well as practicing engineers, engaged with proof assistants. 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.