Finding one. Counting them all.
Imagine a timetable with no clashes. Finding one answers the question “Is this possible?” Counting asks something more: how many different timetables satisfy the rules?
The same distinction appears in coloring maps, matching workers to tasks, and describing configurations of a physical system. Checking a proposed answer can be easy. Counting every answer may demand a very different idea.
Our six-point example is small enough to list every configuration. With 100 points, there are already 2100 on/off patterns. Counting complexity asks: when does the structure let us avoid examining them one by one?
A huge number of possibilities does not by itself make counting hard. With no connections, the answer for n points is simply 2n. The structure of the rules is what matters.
When possibilities carry weight.
Ordinary counting gives every valid answer a contribution of 1. In many models, different answers carry different weights. Adding those contributions gives a partition function.
Return to the six-point cycle. Give each point that is on a weight λ. A configuration with k points on then contributes λk. Move the slider to turn a count into a weighted sum.
Local rules supply contributions; the whole problem sums over assignments. This shared pattern connects questions about constraints, graphs, and networks—and gives their proofs common ground.
Which structures make counting tractable?
An algorithm solves a class of problems. A classification theorem asks a broader question: across a whole family, which cases admit efficient algorithms, and which are #P-hard? CountingLib connects these results and their reusable mathematics across the following directions.
BOOLEAN HOLANT
Local functions. A global sum.
Place a function at each junction of a network, then sum over assignments to its wires. Boolean Holant dichotomies classify the function families that permit efficient evaluation and those that lead to #P-hardness.
COMPLEX-WEIGHTED CSP
Recognizing what the rules allow.
Variables interact through weighted local constraints. The research addresses both the classification of evaluation problems and effective recognition of which case a given collection of rules belongs to.
PLANAR GRAPH HOMOMORPHISMS
How many ways can one graph fit another?
Assign a type to each vertex while respecting which types may be neighbors. Graph coloring is a familiar example. The library includes planar homomorphism dichotomies for nonnegative algebraic weights.
MATCHGATE WIDTH
How compact can an exact representation be?
A complicated counting object may admit a smaller exact representation. Matchgate-width results explore the power and limits of this compression, including qutrit trichotomy and exact compression.
These are introductions to the ideas. The diagrams are schematic; the linked papers and formal sources give the precise assumptions, reductions, and conclusions.
Proofs that other proofs can build on.
A paper explains why a result is true. Lean is a proof assistant: it checks the logical steps of a formal proof against precise definitions and assumptions. Those proofs can then become parts of new results.
CountingLib connects research into a reusable system. Shared definitions describe the objects being counted. Algorithms specify what they compute. Bridge theorems connect models. Classification results retain their precise scope.
Shared foundations
Counts · partitions · encodings · machines
Algorithms & bridges
Variable elimination · interpolation · Pfaffians · reductions
Classification & recognition
Holant · ComplexCSP · PlanarHom · Matchgate Width
Computing the right value and proving a running-time bound are different guarantees. CountingLib states them separately, so the next piece of research can see exactly what it uses and what it assumes.
Further reading
Papers & formalizationsFollow the mathematical statements to their sources. Documentation & APIInstallation, imports, and using the library in your own work. Counting Problems for BabiesAn illustrated introduction, with notes for grown-ups. 38-page PDF.PDF ↗The interactive figures use small browser computations to illustrate the mathematics; they are not Lean-verified executables. The documentation identifies its source snapshot; the repository tracks further development.