Streaming LRAT Certificates into Lean Theorems
TL;DR
The tool lrat-catcher is proposed, which turns a certificate into a Lean theorem, which checks the certificate as a stream while the solver is still running, and supports cube-and-conquer and formulas derived by preprocessing, to still form Lean proofs of the original formula.
Abstract
If the certificate produced by a SAT solver is checked by a verified checker, we get a verdict which convinces. But this verdict cannot be named, reused as a lemma, or composed with other formal developments. We propose the tool lrat-catcher, which turns a certificate into a Lean theorem. It checks the certificate as a stream while the solver is still running. Hence the certificate is not required to be saved to a file. Additionally, our tool makes Lean core's verified LRAT checker resumable so that its state can be serialized. We prove that checking divided at such a state still properly refutes the original formula. We propose two import modes. The stream mode reads the certificate from a pipe in blocks and checks it on the fly in memory. The file mode imports a stored certificate in chunks. If interrupted, it rechecks only the chunks it has not yet completed. The soundness theorem for the stream mode guarantees that a garbled or adversarial stream can only fail the check but not yield a false theorem. We find that with compaction at chunk boundaries, the memory required depends only on the live clause set, not on the certificate size. Our tool supports cube-and-conquer and formulas derived by preprocessing, to still form Lean proofs of the original formula. We provide several end-to-end case studies on well-known combinatorial problems. A larger scaling experiment on the empty-hexagon problem shows that 174 TB of certificates can be imported into Lean via streaming.
