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.

Start Learning Setup Guide

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.

Topics

Foundations

Lattices, polynomials, number theory, probability, complexity theory.

Primitives

Commitments, encryption, signatures, hash functions.

Proof Systems

Sigma protocols, SNARKs, PLONK, folding schemes.

Proof Status Legend

⬚ Stated
◧ Sketched
◨ Partial
✓ Complete
✓✓ Verified