arxivcs.LOcs.AI2026-07-01
LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
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 L…