{"ID":5551731,"CreatedAt":"2026-07-02T01:54:51.863792489Z","UpdatedAt":"2026-07-04T11:27:09.201833898Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.00815","arxiv_id":"2607.00815","title":"LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection","abstract":"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.","short_abstract":"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 th...","url_abs":"https://arxiv.org/abs/2607.00815","url_pdf":"https://arxiv.org/pdf/2607.00815v1","authors":"[\"Stefan Szeider\"]","published":"2026-07-01T11:41:01Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.AI\"]","methods":"[]","has_code":false}