Interactive theorem prover

[Google Scholar] [Wikipedia]

An interactive theorem prover (aka “proof assistant”) is an interactive tool for finding and checking proofs. The search is normally controlled by human provided “tactics”.

Some theorem provers follow the “LCF” theorem prover in generating a proof certificate that is checked by a small trusted core. Some variants optimize this process while preserving the same soundness guarantee.

Annotation burden, Coq theorem prover, HOL theorem prover, Lean theorem prover, PVS theorem prover