Automated proof checking
This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these template messages)
(Learn how and when to remove this template message)

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 handchecking 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
 Computerassisted proof
 Formal verification
 Proof assistant
 Probabilistically checkable proof
 QED manifesto
External links
 Julie Rehmeyer (November 14, 2008). "How to (really) trust a mathematical proof". ScienceNews. Retrieved 20081114.
 Metamath: a proof checking system with an extensive collection of machinereadable proofs covering a considerable range of mathematical fields
 Digimath: Freek Wiedijk's alphabetic list of systems
 MathSystem: Mathematical Software systems
This mathematical logicrelated article is a stub. You can help Wikipedia by expanding it. 