TCSlib
TCSlib is a Lean 4 library for formalizing results in Theoretical Computer Science, built on top of Mathlib. Every theorem is fully machine-verified.
The project is part of UC Berkeley’s URAP program, co-led by Prof. Venkatesan Guruswami and myself. The library is developed by me alongside a group of undergraduate researchers.
Areas currently covered:
- Boolean Function Analysis
- Fourier analysis over the Boolean hypercube
- Hypercontractivity
- Arrow’s theorem
- Error-Correcting Codes
- Singleton, Hamming, Gilbert–Varshamov, and Johnson bounds
- Linear codes
- List decoding
- Quantum codes
