发表机构
Algorithms and Complexity Group, TU Wien（维也纳工业大学算法与复杂性组）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出LRAT-Catcher工具，通过反射运行形式化验证的LRAT检查器，将DIMACS公式和LRAT证书导入Lean4为定理，支持立方与征服求解组合，解决了显式证明项导入的内存问题。
AI 中文摘要
SAT求解器解决了超出交互式定理证明器范围之外的组合问题，并生成LRAT证书以供独立验证。我们提出了LRAT-Catcher，一个独立的通用工具，它将DIMACS公式连同LRAT证书作为定理导入Lean 4。LRAT-Catcher通过反射将来自Lean核心的形式化验证的LRAT检查器作为编译的原生代码运行。这可以扩展到Mathlib的显式证明项导入耗尽内存的实例。LRAT-Catcher还在Lean内部完全组合了立方与征服求解运行。每个立方的反驳与一个覆盖完备性证书（其本身是一个LRAT证明）组合成一个单一的不满足性定理。经过验证的编码将CNF级别的结果连接到原始组合问题。我们使用该工具与Mathlib的证明项导入以及外部检查器cake_lpr进行了评估，将Schur数S(4)=44和Ramsey数R(4,4)=18作为Lean定理建立。
英文摘要
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.
