COUNTING COMPLEXITY IN LEAN

Using CountingLib

Build a checkout or add a pinned source snapshot to your own Lean project. Both use Lean 4.34.1 and the committed dependency locks.

Build a checkout

Install elan, Git, and Python 3.11 or later. The commands below select the source snapshot documented by this preview. The default target builds the core Counting library; larger algorithm and classification collections are optional.

git clone https://github.com/liuchliuch/countinglib.git
cd countinglib
git checkout 6ca34e19e6610f1b785d668d085776129a8e8865
./scripts/lake exe cache get
./scripts/lake build

Use it in another project

In a Lean project using leanprover/lean4:v4.34.1, add this entry to lakefile.toml. The revision pins the existing source snapshot used by this preview. For the published release, use v0.1.0 instead.

Run these Lake commands in your downstream project. Leave CountingLib's own dependency locks unchanged.
Inside a CountingLib checkout, use ./scripts/lake. The wrapper configures the shared module map and clears inherited Lean search paths.

[[require]]
name = "countingComplexity"
git = "https://github.com/liuchliuch/countinglib"
rev = "6ca34e19e6610f1b785d668d085776129a8e8865"

lake update
lake build

Choose the import you need

Counting.Library combines the main aggregates and selected machine adapters. Optional reuse Machine, All, and client layers require explicit imports. Prefer a narrower module when it supplies everything your proof needs.

./scripts/lake build CountingAlgorithms
./scripts/lake build CountingReuse
./scripts/lake build +Counting.Flagships.ComplexCSP

Import	Use
Counting	Core finite counting, encodings, and complexity interfaces
Counting.Model.Basic	Weighted languages and open-instance partitions
Counting.Algorithms	Algorithm and machine interfaces
Counting.Reuse	Intermediate tools and model bridges
Counting.Flagships.Holant	Boolean Holant classification endpoints
Counting.Flagships.ComplexCSP	Complex-weighted CSP endpoints
Counting.Flagships.PlanarHom	Planar homomorphism endpoints
Counting.Flagships.MatchgateWidth	Exact matchgate representation endpoints

Read a theorem with its contract

Search by declaration name, module, or words in the Lean type. Select a module in the left navigation to read related declarations together. Readable signatures are shown directly; full explicit types, specification bodies, and family contracts are available on demand.

A fixed-language polynomial-time theorem fixes its language and representation before runtime instances. A recognizer that receives the language as input has a different contract. Arithmetic operation counts, semantic equalities, exact representation results, and machine bit-time bounds are identified separately.

Use the import shown beside a declaration. An export alias and its canonical provider refer to one kernel declaration.
Check domain, arity, resource, graph-class, and output-codec assumptions before applying a result.
Follow the source link for the complete definition or proof and References for the original paper and Lean release.

Run examples and verification

The tutorial checker compiles fresh client modules and audits their declarations and transitive axioms. Core runs the three introductory examples; all adds the four flagship tutorials and their larger import closures.

Broader algorithms, reuse, and all profiles have larger resource requirements. A successful type export or static website build does not replace Lean compilation and declaration auditing.

python3 scripts/check_examples.py --scope core --workers 2
python3 scripts/check_examples.py --scope all --workers 2

python3 scripts/verify.py --scope core --workers 2