Repository navigation
CountingLib provides reusable counting semantics, reductions, algorithms, and classification theorems in Lean.
This initial release includes the core and optional algorithm/reuse interfaces; Boolean Holant, ComplexCSP, PlanarHom, and Matchgate Width entry points; 15 English guides; three executable tutorials; and references linking research papers to their original Lean sources.
Use Lean 4.34.1 and the committed dependency locks. Add the Lake package countingComplexity at tag v0.1.0, then import Counting or the narrower module you need. See the getting started guide.
Core source and declaration verification, documentation checks, verifier regressions, and all three public tutorials passed in GitHub Actions for this release commit. Broader profile evidence remains the accepted local verification described in the verification guide.
Components retain their individual license scope; no blanket repository-wide license is assigned. See LICENSE.md.
The source archive preserves relative aliases and executable scripts. The documentation ZIP includes the public guides, tutorials, and citation metadata. SHA-256 checksums are supplied alongside both archives.