Proof Assistants and Their Applications in Mathematics and Computer Science

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 prools, 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...