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, low-level 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
