# Streaming LRAT Certificates into Lean Theorems

arXiv: https://arxiv.org/abs/2607.00815 · HTML: https://mlsanity.com/paper/2607.00815/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 33 references that are in the map.
- First posted on arXiv 1 Jul 2026.

## Builds on (most cited first, 9 of 9)

- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Efficient Certified RAT Verification](https://mlsanity.com/paper/1612.02353/) (2016)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Lean-SMT: An SMT tactic for discharging proof goals in Lean](https://mlsanity.com/paper/2505.15796/) (2025)
- [The Resolution of Keller's Conjecture](https://mlsanity.com/paper/1910.03740/) (2019)
- [Efficient Certified Resolution Proof Checking](https://mlsanity.com/paper/1610.06984/) (2016)
- [Happy Ending: An Empty Hexagon in Every Set of 30 Points](https://mlsanity.com/paper/2403.00737/) (2024)
- [Formal Verification of the Empty Hexagon Number](https://mlsanity.com/paper/2403.17370/) (2024)
- [Queen Domination by SAT Solving](https://mlsanity.com/paper/2508.11945/) (2025)

## Abstract (arXiv)

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.