Interactive theorem proving: combine user interaction and automated proof to prove complex properties for which high degree of confidence is relevant.

Justification:

• even careful paper and pencil proofs can be vague and contain errors
• proofs of complex theorems require creativity that is beyond the reach of automated methods

Approaches:

• proof checking: spell out the entire proof using inference system of HOL - tedious, used in Automath, and in early stages of other systems)
• solution: incorporate all automation available (decision procedures, theorem provers, simplifiers, heuristics) into proof checking

Issue with automation:

• automated provers are complex, what if their implementation contains an error?
• need specific provers for specific proofs: if we allow users to write provers, they will cheat and likely make errors

Three approaches to obtaine flexibility, automation, high assurance ('small trusted proof base'):

1. prove correctness of proof procedures (can be harder than prove the problem on which it is used)
2. each proof procedure generates a proof object (checked by simple proof checker) - errors detected late, generating proofs hard, slows down
3. LCF approach: proof procedures create theorems by invoking only basic inference rules - can be slow, but very flexible, can be combined with other two techniques