**Automated proof checking** is the process of using software for checking

proofsIn mathematics, a proof is a convincing demonstration that some mathematical statement is necessarily true. Proofs are obtained from deductive reasoning, rather than from inductive or empirical arguments. That is, a proof must demonstrate that a statement is true in all cases, without a single...

for correctness. It is one of the most developed fields in

automated reasoningAutomated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...

.

Automated proof checking differs from

automated theorem provingAutomated theorem proving or automated deduction, currently the most well-developed subfield of automated reasoning , is the proving of mathematical theorems by a computer program.- Decidability of the problem :...

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 systemThe Mizar system consists of a language for writing strictly formalized mathematical definitions and proofs, a computer program which is able to check proofs written in this language, and a library of definitions and proved theorems which can be referenced and used in new articles. Mizar has goals...

, HOL Light, and

MetamathMetamath is a computer-assisted proof checker. It has no specific logic embedded and can simply be regarded as a device to apply inference rules to formulas...

are examples of automated proof checking systems.

Automated proof checking can be done either as a batch operation, or interactively, as part of a

interactive theorem provingIn computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by man-machine collaboration...

system.

## 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