We present a novel propositional proof tracing format that eliminates complex
processing, thus enabling efficient (formal) proof checking. The benefits of
this format are demonstrated by implementing a proof checker in C, which
outperforms a state-of-the-art checker by two orders of magnitude. We then
formalize the theory underlying propositional proof checking in Coq, and
extract a correct-by-construction proof checker for our format from the
formalization. An empirical evaluation using 280 unsatisfiable instances from
the 2015 and 2016 SAT competitions shows that this certified checker usually
performs comparably to a state-of-the-art non-certified proof checker. Using
this format, we formally verify the recent 200 TB proof of the Boolean
Pythagorean Triples conjecture.

该论文介绍了一种新的命题证明追踪格式，可以消除复杂的处理，从而实现有效（正式）证明检查。通过使用 C 实现证明检查器来证明该格式的好处。然后在 Coq 中形式化命题证明检查的理论，并从形式化中提取出该格式的一个正确性自证明的证明检查器。使用 280 个不可满足的实例对其性能进行了评估，并使用该格式正式验证了布尔勾股三元组猜想的最近 200 TB 的证明。