Chapter 15: Proof Assistants

Proof assistants are software tools that help users write mathematical proofs, with a formal syntax and semantics. In this chapter, we survey some different proof assistants out there.