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.