A proof-assistant is a computer program with which a user can construct completely formal mathematical proofs in some kind of logical system. In contrast to a theorem prover, a proof-assistant cannot find proofs on its own
The Edinburgh Logical Framework is, with De Bruijn's AUTOMATH, one of the two most influential implemented proof representation systems in existence.