This article needs attention from an expert in Mathematics. Please add a reason or a talk parameter to this template to explain the issue with the article. WikiProject Mathematics may be able to help recruit an expert.(February 2009)
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.