TCSlib
TCSlib
A Lean 4 Formalization of
Theoretical Computer Science
TCSlib is an open-source library formalizing results in Boolean Function Analysis and Error-Correcting Codes using Lean 4 and Mathlib. Every theorem is machine-checked.
View on GitHub
Get Started
Boolean Function Analysis
Fourier Analysis on the Hypercube
Foundations of Boolean function analysis over \{-1,1\}^n,
including the Fourier expansion, Parseval's identity, and spectral norms.
Arrow's Impossibility Theorem
A formal proof of Arrow's Theorem via Boolean function analysis: no ranked voting system satisfies independence of irrelevant alternatives, unanimity, and non-dictatorship simultaneously.
Hypercontractivity
The Bonami Lemma and (2,4)-Hypercontractivity inequality,
with applications to the structure of Boolean functions with small Fourier support.
Error-Correcting Codes
Classical Bounds
The Singleton, Hamming, Gilbert–Varshamov, and Johnson bounds on the parameters of error-correcting codes over arbitrary alphabets.
Linear Codes
Formal treatment of linear codes: generator and parity-check matrices, dual codes, and the MacWilliams identity.
Quantum Codes
Quantum Singleton and Quantum Hamming bounds, formalizing the fundamental limits of quantum error correction.
Get Started
TCSlib uses Lean 4 and Mathlib. Install Lean via lean-lang.org/install, then: