math & tcs

### Phase 1: Foundations in Proofs & Pure Mathematics

Before diving into advanced CS theory, you need to develop mathematical fluency—transitioning from computational math (calculus) to structural, proof-based math.

* **Mathematical Rigor & Proof Writing**
* **Focus:** Direct proofs, induction, contradiction, relations, and set theory.
* **Primary Text:** *Book of Proof* by Richard Hammack (Free online) or *How to Prove It* by Daniel J. Velleman.


* **Linear Algebra (Proof-Based)**
* **Focus:** Vector spaces, linear transformations, inner products, spectral theorem (essential for quantum computing and TCS algorithms).
* **Primary Text:** *Linear Algebra Done Right* by Sheldon Axler.


* **Abstract Algebra**
* **Focus:** Groups, rings, fields, and Galois theory (essential for modern cryptography and lattice-based security).
* **Primary Text:** *Abstract Algebra* by Dummit & Foote or *Contemporary Abstract Algebra* by Joseph Gallian.


* **Real Analysis & Measure Theory**
* **Focus:** Metric spaces, sequences, continuity, and formal limits (essential for continuous optimization and formal verification).
* **Primary Text:** *Understanding Analysis* by Stephen Abbott.



---

### Phase 2: Interactive Theorem Proving with Lean 4

Lean 4 bridges code and mathematics by letting you write proofs that are compiler-verified for correctness.

* **Stage 1: Gamified Fundamentals**
* **Resource:** *The Natural Number Game* (Lean 4 Edition).
* **Goal:** Learn how tactics (`induction`, `rw`, `exact`, `simp`) work by building the natural numbers from Peano axioms.


* **Stage 2: Core Lean Programming & Logic**
* **Primary Text:** *Functional Programming in Lean* (FPIL) and *Theorem Proving in Lean 4* (TPIL).
* **Goal:** Understand dependent type theory, the Calculus of Inductive Constructions, and how Lean treats proofs as programs via the Curry-Howard Isomorphism.


* **Stage 3: Formalizing Real Mathematics**
* **Primary Text:** *Mathematics in Lean* (MIL) by Jeremy Avigad et al.
* **Community Hub:** Join the **Lean Zulip Chat**. The Lean community is extremely active, and working through Mathlib (Lean's mathematical library) is the standard way to contribute.



---

### Phase 3: Core Theoretical Computer Science (TCS)

This phase covers classical theoretical CS, exploring what can be computed, how efficiently, and under what guarantees.

* **Automata, Formal Languages & Decidability**
* **Focus:** DFAs, NFAs, Context-Free Grammars, Turing Machines, Halting Problem, Reduction.
* **Primary Text:** *Introduction to the Theory of Computation* by Michael Sipser.


* **Advanced Algorithms & Data Structures**
* **Focus:** Amortized analysis, randomized algorithms, dynamic programming, network flow, NP-hardness.
* **Primary Text:** *Algorithm Design* by Kleinberg & Tardos or *Introduction to Algorithms* (CLRS).


* **Computational Complexity Theory**
* **Focus:** $P$ vs $NP$, $IP=PSPACE$, Polynomial Hierarchy, BQP, BPP, Circuit Complexity.
* **Primary Text:** *Computational Complexity: A Modern Approach* by Sanjeev Arora and Boaz Barak.



---

### Phase 4: Advanced Specializations

Once you have the core theory and Lean mastery, pick 1–2 domain specializations to produce publishable proofs or software tools:

| Domain | Key Focus Areas | Standard Textbooks & Tools |
| --- | --- | --- |
| **Formal Verification & Semantics** | Operational semantics, Hoare logic, type systems | *Types and Programming Languages* (TAPL) by Pierce; *Software Foundations* (Coq/Lean) |
| **Cryptography & ZK-Proofs** | Zero-knowledge circuits, lattices, bilinear maps | *A Graduate Course in Applied Cryptography* by Boneh & Shoup; Circom / Noir |
| **Categorical CS & Type Theory** | Category theory, monads, dependent types | *Category Theory for the Sciences* by Spivak; *Homotopy Type Theory* (HoTT Book) |
| **Quantum Computing** | Quantum circuits, Shor's & Grover's algorithms | *Quantum Computation and Quantum Information* by Nielsen & Chuang |

---

### Practical Portfolio Projects to Prove Mastery

1. **Formally Verify an Algorithm in Lean:** Pick an algorithm from Kleinberg & Tardos (e.g., Dijkstra's, Union-Find, or Red-Black Tree invariant) and write a fully machine-checked proof of correctness in Lean 4.
2. **Write Expository Paper Write-ups:** Take a complex or dense paper (e.g., LWE Cryptography or PCPs) and write a 10–15 page LaTeX document filling in every missing algebraic step.
3. **Contribute to Mathlib:** Submit a PR adding a missing theorem or algebraic structure to Lean's official standard library (`mathlib4`).