count-catcher: Lean Theorems from Model Counting Certificates.

arXiv:2610.36196v1 Announce Type: cross Abstract: We present count-catcher, a tool that turns a CPOG certificate of a count by the exact model counter d4 into a Lean theorem that a CNF formula defined in Lean has exactly N models over V variables. With an enco