count-catcher: Lean Theorems from Model Counting Certificates

Johannes K. Fichte; Stefan Szeider

cs.LOOct 26, 2026

count-catcher: Lean Theorems from Model Counting Certificates

Authors: Johannes K. Fichte, Stefan Szeider

Organizations: Centre de Recherche en Informatique de Lens (CRIL), UMR 8188 Université d’Artois and CNRS, Lens, France · Algorithms and Complexity Group TU Wien, Vienna, Austria

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 encoding lemma, this theorem becomes a theorem about the number of combinatorial objects. A CPOG certificate consists of a Boolean circuit equivalent to the formula and a proof of equivalence. count-catcher checks in Lean that the formula implies the circuit (forward check) and the circuit implies the formula (reverse check). For the forward check, lrat-catcher streams a refutation through the LRAT checker of Lean's standard library. The reverse check and the validity check of the circuit are computations proved correct in Lean. Lean runs all three checks as compiled code, so the theorem depends on Lean's kernel, compiler and runtime, as does CPOG's verified checker. We combine the theorem with results from Mathlib, for instance with Burnside's lemma to count graphs up to isomorphism. We prove the number of Latin squares of order 8 as a weighted sum of hundreds of certified counts from about eight terabytes of certificates. We turn about half of the 2022 Model Counting Competition formulas into theorems, with the three checks taking about a quarter of the time of CPOG's verified checker. We found that CPOG's unverified checker reported wrong counts, and removed its verified checker's dependence on two unproved lemmas. End to end, a theorem costs about the same as a checked count.

Figures & tables

Checker	A run ends in (about)	Verified statement	Trusted beyond the logic
count-catcher	a Lean theorem (a CNF term; the objects)	$\#_{V}(F)=N$ for the term $F$ ; with an encoding lemma, the number of objects	Lean’s compiler and runtime
cpog-lean-check [ 7 ]	an output count (a parsed file)	the checker’s final state implies that the POG is equivalent to the parsed formula and has the computed count	Lean’s compiler and runtime; two unproved lemmas ( Section 4.5 )
cpog-check [ 7 ]	an output count (a parsed file)	none	the C program
SCPOG’s checker [ 8 ]	an output count (a parsed file)	the formula and the circuit agree on the variables that are not projected away, verified down to machine code	the hardware model of CakeML
VeriPB with CakePB [ 34 ]	a HOL4 theorem (the objects)	the number of solutions, obtained by enumerating them	the hardware model of CakeML

Table 1: Checkers for certified model counting and related checkers.

Panel of Figure 1 — Figure 1: A formula $F$ , a POG for it with the counts of its nodes, and its CPOG certificate. The clauses of $F$ have the identifiers 1 and 2; the declaration 3 p 4 -1 2 0 introduces the product node 4 of $\lnot x_{1}$ and $x_{2}$ with the defining clauses 3 to 5, s declares a sum (the two numbers before its 0 are the exclusion hint), r 6 names the root, and an addition a gives the identifier, the clause and, after the first 0 , its hints.

Panel of Figure 2 — Figure 2: From a term to a theorem. Shaded components are untrusted; thick frames are Lean terms and theorems, the double frame the checker, proved sound in Lean and run as native code; the dashed arrow is the path of a formula given as a DIMACS file.

Check	Establishes	Built in Lean	Supplied, untrusted	Checked by
validity	$P$ is a valid POG with count $c(r)$	$P$ and $r$ , parsed from the node table	node table: declarations, exclusion hints	one pass over the node table
forward	$F$ implies the root ( $\Phi$ is unsatisfiable)	$\Phi$ , from $F$ and $P$	additions with hints, keep mask	Lean’s LRAT checker, run by lrat-catcher
reverse	the root implies $F$	implication masks, from $P$ and $F$	none	bit-parallel evaluation

Table 2: The contract of the check.

\Phi

consists of the clauses of

F

, the defining clauses of

P

and the unit clause

\lnot r

; keep mask: Section 4.3 , implication masks: Section 4.4 .

Theorem	Summands	Count	Lean (s)
Composition of certified counts
Triangle-free graphs on 10 vertices, A006785	42	12,172	74.8
Latin squares of order 7	4	$6.15\cdot 10^{13}$	64.0
Latin squares of order 8	737	$1.09\cdot 10^{20}$	325,252
One count as an end-to-end theorem
Dedekind’s number $M(7)$	1	$2.41\cdot 10^{12}$	88.8

Table 3: Theorems about mathematical objects: “Summands” is the number of certified counts in the proof, “Count” the number of objects (for the graphs, of isomorphism classes); for the Latin squares, “Lean” is summed over the certificates and the assembled theorem. † : not listed in the OEIS at time of writing.

Figure 3: The cost of the theorem against CPOG’s checkers on the same d4 outputs. Top : the time of count-catcher over the time of the verified checker per instance, against the size of the full certificate; the line is ratio one. Bottom : medians over the

n

jointly completed runs; “Ratio” is the median per-instance ratio of count-catcher over the verified checker, “Lower” the number of instances on which count-catcher is lower.

Certificate size	$n$	Lean	Check	Memory
below 10 MB	18	86	0.22	37
10 to 100 MB	15	3.9	0.28	12
100 MB to 1 GB	43	0.93	0.20	2.5
above 1 GB	15	0.34	0.22	0.53

Table 4: Medians of the per-instance ratios of count-catcher over cpog-lean-check by the size of the full certificate;

n

is the number of jointly completed runs.

Design choice	Metric	Instances	Median	Range
Deletions left out	certificate bytes	91	2.0	1.1–17
	generation time	75	1.5	0.97–42
Bit-parallel reverse check	vs. top-down evaluation	17	4.6	1.0–17
	vs. sweep per clause	15	90	41–220
Trimmed binary refutation	forward check time	7	1.4	0.71–1.9
Keep mask	Lean time	7	1.2	1.1–1.9

Table 5: Ablation: the median and the range of the factor by which the metric changes without the design choice (above 1: worse); “clauses of

\Phi

loaded” is the percentage of the clauses of

\Phi

that the checker loads with the keep mask. The generation-time factor includes our second patch, applied only to the generator without deletions. The top-down evaluation is our unverified Lean implementation of the strategy of SCPOG’s checker, the sweep per clause our earlier verified reverse check, one bottom-up pass over the POG per clause.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Theorem	Summands	Size	d4	Gen.	Lean	Mem.	Axioms
Composition of certified counts
Triangle-free graphs	42	2.3	25.7	80.8	74.8	9.2	44
Latin squares, order 7	4	0.70	3.8	26.6	64.0	3.9	8
Latin squares, order 8	737	7,929	36,376	486,490	325,252	21.6	1,474
One count as an end-to-end theorem
Dedekind’s $M(7)$	1	1.7	26.2	116.9	88.8	9.3	2

Appendix

Table 6: Resources of the theorems of Table 3 , in the same groups. “Summands” is the number of certified counts, as in Table 3 . “Size” is the total size of the certificates in GB as written by the patched cpog-gen without deletions; for a count of zero it is the size of the LRAT refutation. “d4” is the time of d4 and “Gen.” the time of cpog-gen (for a count of zero, of the SAT solver that refutes the formula), in seconds and summed over the certificates. “Lean” is the Lean time in seconds as in Table 3 . “Mem.” is the peak memory of the Lean process in GB, the largest one if there are several. “Axioms” is the number of native-evaluation axioms that #print axioms lists for the theorem: one per embedded and two per streamed certificate.

Domino tilings
Instance	Count	Size	Gen.	Lean	Mem.
$12\times 12$ board	$5.31\cdot 10^{16}$	500.1	225.4	20.1	3.6
Queens
$n=12$	14,200	406.3	73.9	12.9	3.5
$n=13$	73,712	2,846	461.2	56.0	4.5
$n=14$	365,596	18,194	2,741	302.5	9.3

Appendix

Table 7: The validation families by instance: the number of objects, the size of the certificate in MB as written by the patched cpog-gen without deletions, the generation (“Gen.”) and the Lean time in seconds, and the peak memory (“Mem.”) of the Lean process in GB.

Stage	Reached	Rejected	Timeout	Out of memory	Passed
d4 (4,000 s)	180	–	57	0	123
Generation (4,000 s)	123	–	22	4	97
Translation (4,000 s)	97	–	0	0	97
Lean, theorem stage (3,600 s)	97	0	1	0	96

Appendix

Table 8: The formulas of the competition set by pipeline stage: the formulas that reached each stage and their outcomes, with the time limit of the stage and 64 GB of memory throughout. Only the checker can reject, and “Passed” on its row means proved.

Stage	Outcome	$n$	Formulas
d4	timeout	57	track1_001, track1_003, track1_061, track1_067, track1_085, track1_105, track1_111, track1_115, track1_131, track1_137, track1_139, track1_159, track1_161, track1_163, track1_165, track1_169, track1_173, track1_175, track1_177, track1_179, track1_181, track1_183, track1_185, track1_187, track1_189, track1_191, track1_193, track1_195, track1_197, track1_199, track2_003, track2_065, track2_069, track2_071, track2_075, track2_083, track2_099, track2_105, track2_113, track2_135, track2_141, track2_145, track2_151, track2_153, track2_157, track2_163, track2_171, track2_173, track2_175, track2_177, track2_181, track2_185, track2_187, track2_189, track2_191, track2_193, track2_195
Generation	timeout	22	track1_053, track1_071, track1_075, track1_089, track1_099, track1_107, track1_119, track1_123, track1_125, track1_127, track1_129, track1_143, track1_147, track1_155, track2_001, track2_055, track2_059, track2_119, track2_129, track2_161, track2_179, track2_199
Generation	out of memory	4	track1_151, track2_123, track2_143, track2_169
Lean	timeout	1	track1_083

Appendix

Table 9: The formulas of the competition set that did not become theorems, by the stage and the outcome of Table 8 ;

n

is the number of formulas.

Check	Condition	Constructed	Generated
universe	every variable of $F$ lies in the universe	1	0
	the node table is over the $V$ variables of the theorem	1	0
validity	every argument is an earlier variable	2	2
	the arguments of a product have disjoint supports	3	739,166
	every exclusion hint cites a defining clause of an earlier node	1	31,246
	the exclusion of a sum follows by unit propagation from its hints	3	1,475,770

Appendix

Table 10: Certificates rejected by the checker, counted at the first condition that fails. The rows are in the order in which the checker tests the conditions, with the reverse check before the forward check. The rows “universe” are the two conditions on the universe that the checker tests before the three checks ( Section 4.1 ). “Constructed” are the certificates we built by hand, one or more per condition that violate it, and valid certificates of edge cases (an empty formula, no variables, tautologies only). “Generated” are the certificates of the differential test on small formulas, unmutated or with one mutation each; we do not count the mutants that the translator rejected. In the last two rows we count the accepted certificates and all certificates.

Tool	Version	Source
Lean	4.30.0
Mathlib	commit c5ea003
lrat-catcher	0.2.0
d4	commit 333370c	github.com/crillab/d4
CPOG	release 1.2.0, commit a97ed85	github.com/rebryant/cpog
CaDiCaL [ 4 ]	3.0.1

Appendix

Table 11: The tools of the run of 2026-10-02. From CPOG we used cpog-gen with our two patches, the unpatched cpog-gen for the full certificates, and cpog-check and cpog-lean-check.

Design choice	Metric	Instances	Median	Range
Streamed refutation	check time, same proof	11	0.90	0.82–0.93
	check time, with mask	11	1.9	1.4–2.1

Appendix

Table 12: Embedding the refutation in the theorem file against streaming it, in the format of Table 5 : the median and the range over the instances of the ratio of the check time with the refutation embedded to the check time with it streamed, once for the same refutation in text format and once with the keep mask, inlining and the binary format, which are available only for a streamed refutation.

Reported in	Data	Run	Machine	Limits
Table 3 , Table 6	the runs of the theorems (the five single counts without inlining); order 8: 737 runs, one per certificate, and one for the assembled theorem	2026-10-02; order 8 to 2026-10-04, same pipeline	cpu01; order 8 b5	64 GB, 4 h; order 8 20 or 48 GB per certificate
Table 8 , Table 9	180 runs of the whole pipeline	2026-10-02	b5	d4 and generation 4,000 s, Lean 3,600 s, 64 GB
Figure 3 , Table 4 , Section A.4 , Table 5 deletions	91 runs with both variants of cpog-gen and both CPOG checkers in one job	2026-10-02	b4 (89), b5 (2)	each checker 3,600 s; 32, 48 or 64 GB
Figure 3 , unshortened refutation	91 runs as above, plus a Lean run on the unshortened refutation	2026-10-05	b4	as above
Table 5 bit-parallel reverse check	17 instances, the reverse check alone	2026-10-01; the top-down evaluation of that day	cpu01	1,800 s per check
Table 5 trimmed, keep mask, inlining	7 instances, four translator settings	2026-10-02; certificates of runs before 2026-10-02	cpu01	32 or 64 GB, 2 h

Appendix

Table 13: Provenance of the measured numbers: where each result is reported, the data behind it, the date of the run and the sources where they differ from the run of 2026-10-02, the machine class (cpu01: AMD EPYC 9554P; b4: Intel Xeon E5-2640 v4; b5: AMD EPYC 7402; gpu01: AMD EPYC 9274F) and the limits. We took every measurement once, except for the comparison of streaming with embedding and for the bit-parallel reverse check below 60 s, which we measured three times.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 345 papers

Jul 1, 2026

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 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.

Stefan Szeider

Algorithms and Complexity Group, TU Wien, Vienna, Austria

Lean Theorem Proving Constraint Satisfaction Boolean Satisfiability

Ask PDF

Jun 27, 2026

LAMP: Lean-based Agentic framework with MCP and Proof Repair

Large language models are increasingly capable of mathematical reasoning, but the proofs they generate are often unreliable and hard to verify. Interactive theorem provers such as Lean 4 address this by accepting only kernel-checked proofs; however, their reach is bounded by the formalized knowledge available. While Mathlib, a repository of formalized Lean 4 theorems that covers diverse mathematical areas, certain specialized areas remain underrepresented; notably, the domain of Combinatorics on Words (CoW). CoW studies sequences, exploring their properties such as periodicity, borders, conjugacy, and morphisms. As a result, specialized provers, trained on Mathlib-centered data, lack the lemmas to operate in CoW. We present two contributions. First, we introduce a Lean 4 formalization of CoW containing eight modules and 93 declarations of core definitions and foundational lemmas. Second, we present LAMP, a multi-agent framework that synthesizes kernel-verified Lean 4 proofs by providing explicit, structured domain knowledge at inference time through an ontology, rather than by fine-tuning a prover. LAMP coordinates a Planner, Builder, and Verifier with Model Context Protocol based access to a domain-specific CoW ontology. In a suite of 90 CoW theorems that span all eight modules and three difficulty levels, LAMP synthesizes verified proofs for 96.7% of theorems, substantially exceeding both an unscaffolded baseline and existing specialized provers. An ablation shows that removing LAMP's tool-grounded architecture or its Planner/Builder separation each cost roughly 12 percentage points, even with the backbone model held fixed.

Santhana Srinivasan R, Maithilee Patawar

Indian Institute of Information Technology, Design and Manufacturing, Kancheepuram

Knowledge Augmentation for Language Models Lean Theorem Proving Multi-Agent LLMs

Ask PDF

Oct 26, 2026

KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents

Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organizes language model agents, run by Claude Code, to translate the proofs of a LaTeX paper into the proof assistant Lean 4 with its library Mathlib and check them there, result by result. Each numbered result receives one of four verdicts: verified unconditionally; verified conditionally, with every cited or unproved input stated as a named hypothesis; issue recorded, with its place in the paper and the side at fault; or unfinished, with the reason. The kit follows the paper's own proof step by step, rather than finding a new one. Separate agents write and review, each statement is compared with the paper before it is proved and fingerprinted afterwards, and every verdict rests on evidence that can be rerun without a language model. The kit runs unattended for hours, waits out usage limits, re-checks only what a revision changed and reports its cost by role, model and result. We describe the design, walk through a complete run, and apply the kit to four example papers with answer keys and to three published statistical papers, checked blind in their versions from before public corrections. In all three, the kit found the published error at the step that the correction names, together with further problems that we confirmed by hand. Given the same papers directly, the same language model working with Lean classified fewer results correctly on the longest paper and reported some statements narrower than the paper's as proved; no verdict of the kit claimed more than its Lean evidence showed.

Zihua She, Xiao Wang

Department of Statistics, Purdue University, West Lafayette, IN 47907, USA

Large Language Model-Guided Theorem Proving Automated Theorem Proving

Ask PDF

Abstract

Formal Verification

Explore similar work

LRAT-Catcher: Importing SAT Solver Certificates into Lean4 by Reflection

LAMP: Lean-based Agentic framework with MCP and Proof Repair

KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents