TCSlib
A Lean 4 library for Theoretical Computer Science.
Official website at https://shilun-allan-li.github.io/tcslib/.
What's TCSlib?
TCSlib formalizes results in Theoretical Computer Science using Lean 4 and Mathlib. Every theorem is machine-checked.
Reading the sources without a Lean background? lean-glossary.md
briefly explains the Lean and Mathlib jargon (fuel, Sigma, Prop vs Bool, naming
conventions, …) that appears in declaration names and docstrings.
For a catalog of the models of computation the library formalizes — Turing machines,
circuits, formulas, decision trees — and the conversions between them, see
TCSlib/ComputationalModels.lean.
Areas covered
- Boolean Function Analysis — Fourier analysis over the Boolean hypercube, hypercontractivity, Arrow's theorem, and more.
- Error-Correcting Codes — Singleton, Hamming, Gilbert–Varshamov, and Johnson bounds; linear codes; list decoding; quantum codes.
Using TCSlib in your project
To add TCSlib as a dependency, add the following to your lakefile.lean:
require TCSlib from git "https://github.com/Shilun-Allan-Li/tcslib" @ "main"
The theorem dataset
dataset/tcslib_theorems.jsonl.gz pairs every blueprint-bound theorem with a
self-contained informal statement, a standalone formal statement, a flattened proof file,
a difficulty rating and its provenance (textbook citation or an informalized account of
the proof). After formalizing something, put the text it came from under
blueprint/src/references/ and run python3 scripts/dataset_pipeline.py --yes: it
ingests new texts, matches every text the blueprint does not cite yet, and carries the
new declarations into the dataset incrementally, on the Claude Code or the OpenAI Codex
CLI. python3 scripts/sources.py shows which texts are attached, which theorems they
cover and which texts are still missing. See dataset/INSTRUCTIONS.md
for the short version, dataset/DESIGN.md for the design and its rules,
and dataset/README.md for the whole builder.
Matching PDF proofs to TCSlib
The repository includes an auditable Claude Code workflow for comparing a local
PDF or validated Markdown reference with TCSlib proofs. Agent stages run through
headless claude -p with --json-schema structured output (the claude CLI
must be installed and authenticated); model tiers are configured in
proofmatch/agents.py (DEFAULT_MODEL / COMPARE_MODEL, default
claude-opus-4-8) with matching prices in proofmatch/budget.py:
# Free local extraction only
python3 scripts/proofmatch.py extract notes.pdf --local-only
# Estimate before paid agent stages
python3 scripts/proofmatch.py estimate notes.pdf
# Full extraction, selective visual repair, search, and comparison
python3 scripts/proofmatch.py run notes.pdf
# Start downstream matching from existing validated Markdown
python3 scripts/proofmatch.py match notes.md
Runs are uncapped by default, so no stage is skipped for want of budget; spend
is still tracked and reported. --max-cost N optionally caps estimated spend
(capped runs degrade gracefully and persist partial reviews). Verdicts: same (proof matches →
\proofsource + \proofstep), method_divergence (statement in the text,
different proof → \statementsource), not_in_text (too granular for the text
or a bare exercise → queued in informalize_queue.md for a later LLM pass that
informalizes the Lean proof), different, uncertain.
The workflow stores both notes.raw.md and notes.md. It writes no blueprint
proof-source metadata until the user explicitly approves a generated review with
python3 scripts/proofmatch.py review RUN_ID.
Then run lake update to fetch the dependency.
Building locally
Install Lean following the setup instructions, then run:
lake exe cache get
lake build
Contributing and discussion
Contributions are welcome — please open an issue or pull request on GitHub.