LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection
2026-07-01 • Logic in Computer Science
Logic in Computer ScienceArtificial Intelligence
AI summaryⓘ
The authors present LRAT-Catcher, a tool that helps verify solutions to complex logic puzzles inside the Lean 4 theorem prover. Instead of using too much memory with direct proof imports, LRAT-Catcher efficiently checks proofs by running verified code directly. It also handles a solving method called cube-and-conquer entirely within Lean, combining small pieces into one big proof. They tested the tool by verifying famous problems like the Schur and Ramsey numbers as formal theorems in Lean.
SAT solverLRAT certificateLean 4theorem proverDIMACS formatcube-and-conquerproof verificationMathlibSchur numberRamsey number
Authors
Stefan Szeider
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.