Different ways of proving theorems with a computer:

Automatic theorem provers find complete proofs on their own

Huge amount of work, beginning in the AI community in the 50s to 80s

In limited domains, extremely successful (e.g., hardware model checking)

In general, though, this approach is just too hard

Proof checkers simply verify proofs that they are given

These proofs must be presented in an extremely detailed, lowlevel form

Proof assistants are hybrid tools

"Hard steps" of proofs (the ones requiring deep insight) are provided by a human

"Easy parts" are filled in automatically