Automated proof checking

This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (August 2012)

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 (or its Portal) 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.

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[edit]

External links[edit]

Julie Rehmeyer (Friday, November 14, 2008). "How to (really) trust a mathematical proof". ScienceNews. Retrieved 2008-11-14.
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