Learn Cryptography with Formal Proofs
A living textbook where every definition is precise, every theorem references its source, and proofs are machine-verified in Lean 4.
What Makes This Different
Precise Definitions
Every concept is defined in Lean 4, eliminating ambiguity. The code is the specification.
Paper References
Every theorem cites its source paper. Follow the research trail from textbook to cutting-edge results.
Transparent Status
Each result shows its formalization status: stated, sketched, partial, complete, or verified.
Interactive Learning
Run Lean code in your browser. Experiment with definitions and explore proofs interactively.