## Some thoughts on proof assistants

A proof assistant is a computer program that takes as input a proof in a formal language and outputs true if and only if the proof is a valid proof in a formal system. An example would be first-order logic with its inference rules. Proof assistants are supposed to tell you whether your proof is […]