A “Proof Assistant” is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness.

I will outline how Proof Assistants work, how they are used to verify mathematical proofs and computer systems. Verifying a proof with a PA is a lot of work, but as mathematical proofs get more and more difficult and complex there is an increasing use of PAs for mathematical proofs. Also for critical computer components it will pay off to verify them completely using a PA.

We will discuss why one would trust a PA and their limitations in use, which basically rest on the limitations of proof automation. It has recently become clear that Machine Learning provides methods that apply very well to speeding up proof automation.