A proof checker is a program that takes a claimed proof of a logic formula and decides whether this claim is true; in applications such as program verification and automated reasoning, it is thus not necessary to trust the (potentially big) prover but only the (comparatively small) checker. However, since machine-checkable proofs can get very large, it is necessary to only represent the essential structure of a proof and let the checker regenerate the missing parts.

This paper presents the main results of the ProofCert project, which applies logic programming to proof checking based on three key ideas. The first one is the proof system LKF, where a formula is annotated by a polarity that indicates how logic inference rules have been applied in proving the formula; this reduces the amount of search that has to be performed in the proof reconstruction. The second one is to augment the proof by certificates, extra information that further simplifies the reconstruction process. The third one is to design the inference system in such a way that it represents an executable program in the logic language lambdaProlog, thus ensuring the soundness of the checker.

The paper succeeds in conveying the main results of ProofCert to nonexperts in the field. While the ideas indeed seem very promising, the conclusions point out that a critical point for the practical adoption of the approach will be the development of effective implementation techniques for lambdaProlog that allow for checking huge proofs without compromising logical soundness.