将SAT求解器证书导入Lean4，自动验证组合问题的数学结论。
LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
- 通过反射机制调用形式化验证的LRAT检查器，导入证书并生成定理。
- 成功证明舒尔数S(4)=44和拉姆齐数R(4,4)=18，内存消耗显著更低。
- 适合需要形式化验证复杂组合结果的研究者使用。
SAT求解器能解决交互式定理证明器无法处理的组合问题，并生成可用于独立验证的LRAT证书。我们提出LRAT-Catcher，一个独立通用工具，可将DIMACS格式公式与LRAT证书导入到Lean 4中作为定理。该工具通过反射调用已形式化验证的Lean核心中的LRAT检查器，以编译后的原生代码运行。该方法可扩展至Mathlib显式证明项导入时内存耗尽的实例。此外，LRAT-Catcher可在Lean内部完整执行cube-and-conquer求解流程：每立方体的反驳通过覆盖完备性证书（本身是LRAT证明）合并为单一不可满足性定理。经验证编码将CNF层面的结果与原始组合问题关联。我们在建立舒尔数S(4)=44和拉姆齐数R(4,4)=18为Lean定理上，对比了Mathlib的证明项导入与外部检查器cake_lpr，验证了其有效性。
原文摘要 · Abstract (English)
SAT solvers settle combinatorial problems beyond the reach of interactive theorem provers and produce LRAT certificates for independent verification. We present LRAT-Catcher, a standalone, general-purpose tool that imports a DIMACS formula together with an LRAT certificate into Lean 4 as a theorem. LRAT-Catcher runs the formally verified LRAT checker from Lean core as compiled native code via reflection. This scales to instances where Mathlib's explicit proof-term import exhausts memory. LRAT-Catcher also composes cube-and-conquer solving runs entirely inside Lean. Per-cube refutations are combined with a cover-completeness certificate, itself an LRAT proof, into a single unsatisfiability theorem. Verified encodings connect CNF-level results to the original combinatorial problems. We evaluate the tool against Mathlib's proof-term import and the external checker cake_lpr on establishing the Schur number S(4) = 44 and the Ramsey number R(4,4) = 18 as Lean theorems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。