# Approaches to Reliable Complex Proofs

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'):

- prove correctness of proof procedures (can be harder than prove the problem on which it is used)
- each proof procedure generates a proof object (checked by simple proof checker) - errors detected late, generating proofs hard, slows down
- 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