Automated proof checking

Automated proof checking is the process of using software for checking proofs for correctness. It is one of the most developed fields in automated reasoning.

Automated proof checking differs from automated theorem proving in that automated proof checking simply mechanically checks the formal workings of an existing proof, instead of trying to develop new proofs or theorems itself. Because of this, the task of automated proof verification is much simpler than that of automated theorem proving, allowing automated proof checking software to be much simpler than automated theorem proving software.

Because of this small size, some automated proof checking systems can have less than a thousand lines of core code, and are thus themselves amenable to both hand-checking and automated software verification.

The Mizar system, HOL Light, and Metamath are examples of automated proof checking systems.

Automated proof checking can be done either as a batch operation, or interactively, as part of an interactive theorem proving system.

Field journals and conferences

• Intelligent Computer Mathematics
• Journal of Formalized Reasoning
• Interactive Theorem Proving
• Formalized Mathematics
• Studies in Logic, Grammar and Rhetoric

See also

• Computer-aided proof
• Formal verification
• Proof assistant
• QED manifesto

External links

• Metamath: a proof checking system with an extensive collection of machine-readable proofs covering a considerable range of mathematical fields
• Digimath: Freek Wiedijk's alphabetic list of systems
• MathSystem: Mathematical Software systems