Streaming LRAT Certificates into Lean Theorems

תקציר מקורי באנגליתarXiv:2607.00815v2 Announce Type: replace-cross 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