count-catcher: Lean Theorems from Model Counting Certificates

1 Introduction

• The motivation for machine-checkable counts includes earlier errors: cpog-check reported a wrong count on 7 of 91 certificates.The paper also describes historical corrections to published counts, including counts of reduced Latin squares and closed knight’s tours.Source: §1 · p. 2
• Latin squares of order 8 are counted as a weighted sum over cycle types of the second row, which in a reduced square (identity first row and column) is a symbol permutation.Up to isomorphism, exactly one graph on 13 vertices has neither a triangle nor five mutually nonadjacent vertices; it is the circulant graph with jumps 1 and 5.Source: §1 · p. 3
• Certificates for the order-8 Latin-square count total 7.9 TB, with up to 32.7 GB each, so a single proof term is too large for the kernel to process.The count is split into 737 certificates by cycle type and three cells of the third row.Source: §1 · p. 3
• The proof chain uses an encoding lemma, forward and reverse implications between the formula and circuit, a circuit-validity check, and arithmetic.The forward check streams an LRAT refutation through Lean’s checker; the reverse and validity checks are computations proved correct in Lean.Source: §1 · p. 3
• The theorem relies on Lean’s kernel, compiler, and runtime because Lean runs all three checks as compiled code.The same trusted base applies to CPOG’s verified checker.Source: §1 · p. 3
• Count-catcher turns a CPOG certificate into a theorem that a Lean formula has exactly N models over V variables; an encoding lemma then connects that count to objects.The certificate supplies data to check, while Lean builds the theorem’s components.Source: §1 · pp. 2–3
• Count-catcher is tested against enumeration on more than twelve million generated and mutated certificates.The tool also shortens the refutation in three untrusted steps before the forward check.Source: §1 · pp. 3–4
• 96 of 180 Model Counting Competition formulas become theorems, and the three checks take about a quarter of the time of CPOG’s verified checker.The unverified cpog-check reports wrong counts; the authors also remove the verified checker’s dependence on two unproved lemmas.Source: §1 · p. 4

2 Related Work

• Count-catcher obtains an exact model count without enumeration as a theorem about a proof-assistant term, unlike enumeration-based proof logging, which is infeasible for counts as large as the order-8 Latin-square count.CPOG’s checker theorem concerns the parsed DIMACS file and does not connect that count to a Lean term or the counted objects.Source: §2 · p. 4
• CPOG provides the certificate format, generator, and Lean-verified checker used here; SCPOG extends the format to projected counting but does not guarantee a count.Other cited systems include MICE, CD4, kcps, CLIP, and ApproxMCCert, which certifies approximate counts.Source: §2 · p. 4
• Lean theorems have also been obtained by checking refutations, while count-catcher uses a certificate to establish an exact count theorem about a term.The related approaches include proof by reflection, LRAT checking, and verified graph search.Source: §2 · pp. 4–5
• Sequencelib contains more than 25,000 OEIS sequences, and count-catcher proves large values of such sequences.For counting finite structures up to isomorphism, the paper contrasts complete symmetry breaking with using Burnside’s lemma to sum certified counts.Source: §2 · p. 5

• The model count #V(F) counts assignments to all V variables, including variables absent from clauses, so the universe is part of the statement.A variable absent from every clause doubles the count.Source: §3 · p. 5
• A POG is a directed acyclic circuit with literal leaves and product (AND) and sum (OR) nodes, whose supports determine how node counts are computed.Product arguments must have disjoint supports, and sum arguments must exclude each other.Source: §3 · pp. 5–6
• CPOG certificates declare circuit nodes with Tseitin clauses, then use additions to prove the formula implies the root and deletions to prove the root implies the formula.Sum declarations include an exclusion hint; additions use reverse unit propagation hints.Source: §3 · p. 6
• An LRAT refutation can be checked by Lean’s verified LRAT checker to prove a CNF formula unsatisfiable.Oversized refutations can be streamed in blocks during evaluation.Source: §3 · p. 6

4 From Certificate to Theorem

• The count theorem composes the user-provided encoding lemma with checks of formula–POG equivalence, POG count, and arithmetic yielding N.The chain begins with the equality between the number of encoded objects and the formula’s model count.Source: §4 · p. 6

4.1 The Theorem and the Contract

• The theorem states a count for a Lean formula term; untrusted translation failures can make checks fail but cannot produce a false theorem.For a formula supplied only as DIMACS, the theorem uses a Lean parser, which must be trusted when interpreting it as the benchmark instance.Source: §4.1 · p. 7

4.2 The Validity Check

• The validity check verifies node references, disjoint product supports, and mutually exclusive sum arguments while computing each node’s support and count.The checker also checks that formula variables and the node table use the declared universe size.Source: §4.1 · p. 7, §4.2 · p. 8

4.3 The Forward Check

• The forward check reduces formula-implies-root to an LRAT refutation of the formula clauses, circuit definitions, and ¬root, with Lean constructing that target itself.The translator may trim and inline refutation additions; a keep mask can select only a subset of Lean-generated clauses.Source: §4.3 · p. 8

4.4 The Reverse Check

• The reverse check tests whether the POG root implies every formula clause, propagating implication masks for batches of 63 clauses in one machine word.Its soundness follows from an invariant that each set mask bit denotes an implication; in the accepted fragment, the converse also holds.Source: §4.4 · pp. 8–9

4.5 Design Rationale and Trusted Base

• Reflecting CPOG’s verified checker would not directly give the needed formula count, so count-catcher adds validity and reverse checks and a composition theorem.The theorem depends on Lean’s kernel, standard axioms, compiler and runtime, and native-evaluation axioms; streamed refutations require trusting that native code returns each block exactly once.Source: §4.5 · p. 9
• Tests rejected certificates violating individual check conditions, and differential testing accepted only correct counts among more than twelve million generated and mutated certificates.The authors also removed the archived cpog-lean-check build’s dependence on two unproved lemmas by proving those lemmas directly.Source: §4.5 · p. 9

5.1 Encoding Lemmas

• An encoding lemma gives a bijection between formula models over the universe and the object type, allowing a checked formula count to establish the object cardinality.The shared card_of_check lemma converts the model-count theorem into Nat.card X = N.Source: §5.1 · p. 9
• For a new family, users supply an encoder and encoding lemma; the Latin-square order-7 encoder uses cell, row, and column exactly-one clauses and fixes the first row and column.The reduced squares are split into second-row fibers, each counted through count-catcher; the listed theorem file is generated rather than handwritten.Source: §5.1 · p. 10

5.2 Composition by Symmetry

• 12,172 triangle-free graphs on ten vertices up to isomorphism are proved by combining 42 certified fixed-point counts through Burnside’s lemma.The proof verifies the cycle-type list and weighted sum in Lean.Source: §5.2 · pp. 10–11
• For graph actions, each cycle-type summand multiplies its class size by a fixed-point model count, obtained by adding clauses for variables moved by the permutation.For Latin squares, fiber counts depend only on second-row cycle type; order 8 further splits fibers using unit clauses on three cells of the third row, whose parts are proved to sum to the fiber.Source: §5.2 · pp. 10–11

• Dedekind’s number M(8) was out of reach for d4 in the probes, while a single certificate for Latin squares of order 7 exceeded 64 GB, so the authors split by fibers.Source: §6 · p. 11
• 737 certified counts assembled latin8_all in 90 hours of Lean time, and the count was checked against the literature.Source: §6 · p. 11
• Ganak and SharpSAT-TD returned the same four integers as the pipeline on the four reported OEIS formulas.For even torus-grid size, the formula splits into two independent halves, making A303210(10) cheaper than A303210(9).Source: §6 · p. 12
• Certified counts support the result that exactly one isomorphism class of the specified 13-vertex Ramsey graphs exists.The count of one is used as the uniqueness theorem’s hypothesis, alongside a separate check that Mathlib’s circulant graph with jumps 1 and 5 belongs to the class.Source: §6 · p. 12
• 96 of 180 competition formulas became theorems; with a 10,000-second generation limit, 104 became theorems.The comparison reports 111 of 123 formulas solved by d4 verified with CPOG’s generator and unverified checker under a different time limit.Source: §6 · p. 12
• About the same median time was needed for the theorem pipeline and checked-count pipeline; Check took about a quarter of cpog-lean-check’s time, and above 1 GB the Lean process took about a third.The figure compares per-instance runtime ratios against certificate size; the table reports medians by certificate size.Source: Figure 3 · p. 13, §6 · pp. 13–14, Table 4 · p. 13
• Both checkers accepted every certificate, but cpog-check reported a wrong count on 7, while cpog-lean-check reported the correct count on every one.The reported cause was a fault in rational-number normalization.Source: §6 · p. 14
• Omitting deletions halves certificate size in the median, and the bit-parallel reverse check has a large effect.For a 4 × 4 domino board, kernel-only checking took 24 s versus 16 ms natively; on the 6 × 6 board it exceeded 64 GB.Source: §6 · p. 14, Table 5 · p. 14

7 Conclusion

• count-catcher turns a CPOG certificate into a Lean theorem about a formula as a term, and an encoding lemma connects it to a count of objects.The trusted base includes Lean’s kernel, compiler, and runtime; d4 with cpog-gen is the current front end.Source: §7 · p. 14
• cpog-gen limits which counts can be proved and takes longer to generate the refutation than d4 takes to generate the count.Source: §7 · p. 14
• Weighted counts require changes to the validity check and count theorem, while projected counts also require changing the reverse check.The paper also identifies writing refutations during counter search and splitting counts by cubes as possible extensions.Source: §7 · p. 14

A.1 Resources of the Theorems about Mathematical Objects

• The largest order-8 Latin-square certificate is 32.7 GB.Source: §A.1 · p. 20
• Table 6 reports certificate size, d4 and generator time, Lean time, peak Lean memory, and native-evaluation axioms for theorem groups.For Latin squares, memory is reported as the largest peak among the Lean processes for individual certificates and the assembled theorem.Source: Table 6 · p. 20, §A.1 · p. 20

A.2 Validation Families

• Validation-family counts agree with OEIS sequences for domino tilings, queens, and grid independent sets, and with two counters for graphs.The graph comparisons are with ganak and SharpSAT-TD.Source: §A.2 · p. 20

A.3 The Competition Set

• Bryant et al. report that d4 completed 123 of 180 formulas within 4,000 seconds and their toolchain fully verified 111 of those 123.Their experiments also used a 90-formula subset where d4 took under 1,000 seconds and POGs had at most 107 defining clauses.Source: §A.3 · pp. 20–21
• Table 8 organizes competition formulas by pipeline stage and outcome, with stage time limits and 64 GB of memory throughout.Only the checker can reject a formula; “Passed” on its row means proved.Source: Table 8 · p. 21
• On a rerun with a 10,000-second generation limit, 10 of 26 previously failed formulas generated certificates and 8 became theorems within Lean’s 3,600-second limit.All 10 generated certificates within the 10,000-second limit.Source: §A.3 · p. 21
• cpog-gen failed on 26 formulas; among 25 with a written POG, 20 had more than 107 defining clauses.Four formulas exceeded the memory limit, and d4 took more than 2,800 seconds on them.Source: §A.3 · p. 21

A.4 The Smallest Miscount of cpog-check

• 8,281,581,627,129,036,755 was cpog-check’s count for random cubic, 100 vertices, versus 8,281,581,627,129,350,099 proved by count-catcher and reported by d4 and cpog-lean-check.This was the smallest count among the seven wrong counts in 91 certificates compared with CPOG’s checkers.Source: §A.4 · p. 21
• The error came from normalizing a rational by a power of 2 or 5 dividing its lowest base-109 digit, which need not divide the number, and discarding the remainder.The fault was in q25.c.Source: §A.4 · p. 22
• After limiting that power to at most the ninth, cpog-check returned correct counts on every retested certificate, including the seven miscounts.The authors reported the fault and one-line fix to CPOG’s developers.Source: §A.4 · pp. 21–22

A.5 Constructed Certificates and the Differential Test

• Every accepted certificate in the differential test had the count obtained by enumeration, across small formulas and certificates tested in embedded, streamed, and default configurations.d4 and patched cpog-gen generated certificates; each was mutated in one place, and translator-rejected mutants were excluded.Source: §A.5 · p. 22

A.6 The Bit-Parallel Reverse Check

• The reverse check processes batches of at most 63 clauses using bit masks that track which literals and circuit nodes imply each clause.Products combine argument masks with bitwise OR, while sums combine masks with bitwise AND; the root must imply each non-tautological clause.Source: §A.7 · p. 23

A.7 Soundness Theorems

• The soundness theorems connect certificate validity, forward and reverse checks, and streamed LRAT refutations to the final model-count theorem.The listed axioms are propositional extensionality, choice, and quotient soundness; the kernel-checked definitions and compiled C code are built from the same source, but Lean does not check their agreement at load time.Source: §A.7 · pp. 22, 24

A.8 Provenance of the Measurements

• The checker comparison omits 14 competition formulas with the longest generation times, including three that exceeded cpog-lean-check’s 64 GB memory limit in an earlier run.On the largest included certificate, track2_011 at 6.7 GB, cpog-lean-check took 519.9 s and 24.2 GB, while the Lean process took 184.7 s and 6.8 GB.Source: §A.8 · p. 25
• The ablation tests use selected instances: the bit-parallel reverse check includes 11 instances and six competition formulas on which an earlier reverse check was slow.Other comparisons likewise use specified instance subsets, including streaming versus embedding on 11 instances.Source: §A.8 · p. 25, Table 12 · p. 25
• The measurement provenance records run data, dates, machines, and limits; the patched generator omits deletions and frees unused proof clauses, shortening solver proofs of at least 500 clauses with drat-trim.The provenance table’s measurements were generally taken once, with specified exceptions.Source: §A.8 · p. 25, Table 13 · p. 26