Learn Lean 4

Master the essentials of Lean 4 needed to understand and contribute to Cryptography Academy's formal proofs.

Why Learn Lean?

Every definition and theorem on this site is written in Lean 4. Understanding Lean lets you read the precise mathematical definitions, verify proofs yourself, and contribute new formalizations. You don't need to become an expert—just enough to follow along.

Setting Up Lean

You can try Lean directly in your browser using the interactive editors on this site. For a full development environment, follow these steps:

1 Install elan (Lean version manager)

elan manages Lean toolchains, similar to rustup for Rust. 

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

On Windows, download and run elan-init.exe.

2 Install VS Code + Lean 4 extension

VS Code provides the best Lean editing experience with real-time feedback, goal display, and Unicode input.

  1. Install VS Code
  2. Install the lean4 extension

3 Clone the Cryptography Academy project

Get the formalized proofs and run them locally. 

git clone https://github.com/cryptographyacademy/cryptographyacademy.github.io.git
cd cryptographyacademy.github.io
./scripts/setup-lean.sh

This installs the correct Lean version and downloads the Mathlib cache.

4 Build and check proofs

Use Lake (Lean's build system) to compile and verify the proofs. 

# Build the entire project
cd lean
lake build

# Or use the Makefile from the project root
make build

Common Lake commands:

  • lake build — Compile all Lean files and check proofs
  • lake exe cache get — Download pre-built Mathlib (faster than compiling)
  • lake clean — Remove build artifacts

No installation needed? The tutorials include interactive editors powered by lean4web. You can learn and experiment without installing anything.

Learning Path

📖

1. Reading Lean Code

Learn to read definitions, theorems, and proofs. Understand the syntax without writing code yourself.

Start here →
🧱

2. Types and Terms

Understand Lean's type system—the foundation of formal mathematics. Learn about Prop, Type, structures, and inductive types.

20 min read
🔍

3. Proofs and Tactics

How proofs work in Lean. Learn common tactics like intro, apply, exact, and how to read tactic proofs.

25 min read
📚

4. Using Mathlib

Navigate Mathlib's algebraic structures: groups, rings, fields. Find and use existing theorems for your proofs.

30 min read
🔐

5. Cryptographic Patterns

Common patterns in cryptographic formalizations: security definitions, game-based proofs, and computational assumptions.

35 min read

External Resources

For deeper learning, these official resources are excellent: