sdiehl/zero-to-qed

From Zero to QED: An informal introduction to formality with Lean 4

Lean

126

283 commits

updated Sep 6, 2026

sdiehl.github.io/zero-to-qed

See the code

README

From Zero to QED

An informal introduction to formality in Lean 4.

Read

HTML - Read online
PDF - Download for offline reading

Get Started

Follow the official Lean installation instructions.

#	Prose	Code
1	Introduction
2	Why?
3	Theorem Provers
4	Basics	Basics.lean
5	Lake Build System
6	Data Structures	DataStructures.lean, MagicTheGathering.lean
7	Control Flow and Structures	ControlFlow.lean, FizzBuzz.lean, Collatz.lean, DndCharacter.lean
8	Termination and Well-Founded Recursion	Termination.lean
9	Standard Library and Batteries	StdLibrary.lean
10	Polymorphism and Type Classes	Polymorphism.lean, SpellEffects.lean, Units.lean
11	Effects	Effects.lean, ATM.lean
12	IO and Concurrency	IO.lean, WordFreq.lean
13	Proofs	Proving.lean
14	Type Theory	TypeTheory.lean
15	Dependent Types	TypeTheory.lean, DependentTypes.lean, VendingMachine.lean, NQueens.lean
16	Proof Strategy	ProofStrategy.lean
17	Congruence and Subtyping	Subtyping.lean
18	Classic Proofs	Proofs/
19	Algebraic Structures	AlgebraicStructures.lean
20	Mathlib	Mathlib.lean
21	Verified Programs	Verification.lean, Compiler.lean, GameOfLife.lean, StackMachine.lean, CircuitBreaker.lean, ParserCombinators.lean
22	Model Checking	ModelChecking.lean
23	Artificial Intelligence
24	References

Contributing

See BUILD.md for details on the HTML and PDF build pipeline. Add yourself to CONTRIBUTORS.md and submit a PR.

License

Software (Lean code in src/): MIT License. See LICENSE.

Prose (text in docs/): Public domain. Share it, adapt it, translate it. I just ask that you not sell it. It is meant to be free.

formal-methods

lean

Contributors

240 commits

20 commits

5 commits

3 commits

Similar repos

lean-ja/lean-by-example

コード例で学ぶ Lean 言語

188

anqur/TinyLean

Tiny theorem prover with syntax like Lean 4 in <1K LOC

leanprover/lean

Lean Theorem Prover

2,154

plfa/plfl

Programming Language Foundations in Lean

lean-forward/logical_verification_2024

The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

BaDaaS/lean4-courses

SatyendraBanjare/plt-formal-methods-resources

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language…

hrmacbeth/math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

372

Languages

Lean

86.8%

Python

12.5%

sdiehl/zero-to-qed

From Zero to QED: An informal introduction to formality with Lean 4

Lean

126

283 commits

updated Sep 6, 2026

sdiehl.github.io/zero-to-qed

See the code

README

From Zero to QED

An informal introduction to formality in Lean 4.

Read

HTML - Read online
PDF - Download for offline reading

Get Started

Follow the official Lean installation instructions.

#	Prose	Code
1	Introduction
2	Why?
3	Theorem Provers
4	Basics	Basics.lean
5	Lake Build System
6	Data Structures	DataStructures.lean, MagicTheGathering.lean
7	Control Flow and Structures	ControlFlow.lean, FizzBuzz.lean, Collatz.lean, DndCharacter.lean
8	Termination and Well-Founded Recursion	Termination.lean
9	Standard Library and Batteries	StdLibrary.lean
10	Polymorphism and Type Classes	Polymorphism.lean, SpellEffects.lean, Units.lean
11	Effects	Effects.lean, ATM.lean
12	IO and Concurrency	IO.lean, WordFreq.lean
13	Proofs	Proving.lean
14	Type Theory	TypeTheory.lean
15	Dependent Types	TypeTheory.lean, DependentTypes.lean, VendingMachine.lean, NQueens.lean
16	Proof Strategy	ProofStrategy.lean
17	Congruence and Subtyping	Subtyping.lean
18	Classic Proofs	Proofs/
19	Algebraic Structures	AlgebraicStructures.lean
20	Mathlib	Mathlib.lean
21	Verified Programs	Verification.lean, Compiler.lean, GameOfLife.lean, StackMachine.lean, CircuitBreaker.lean, ParserCombinators.lean
22	Model Checking	ModelChecking.lean
23	Artificial Intelligence
24	References

Contributing

See BUILD.md for details on the HTML and PDF build pipeline. Add yourself to CONTRIBUTORS.md and submit a PR.

License

Software (Lean code in src/): MIT License. See LICENSE.

Prose (text in docs/): Public domain. Share it, adapt it, translate it. I just ask that you not sell it. It is meant to be free.

formal-methods

lean

Similar repos

lean-ja/lean-by-example

コード例で学ぶ Lean 言語

188

anqur/TinyLean

Tiny theorem prover with syntax like Lean 4 in <1K LOC

leanprover/lean

Lean Theorem Prover

2,154

plfa/plfl

Programming Language Foundations in Lean

lean-forward/logical_verification_2024

The Hitchhiker's Guide to Logical Verification and Associated Materials (2024 Edition)

BaDaaS/lean4-courses

SatyendraBanjare/plt-formal-methods-resources

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language…

hrmacbeth/math2001

Lecture notes for a course on writing proofs, on paper and in the Lean proof assistant

372

Contributors

240 commits

20 commits

5 commits

3 commits

Languages

Lean

86.8%

Python

12.5%

sdiehl/zero-to-qed

README

From Zero to QED

Read

Get Started

Contents

Contributing

License

Contributors

Similar repos

Languages

sdiehl/zero-to-qed

README

From Zero to QED

Read

Get Started

Contents

Contributing

License

Similar repos

Contributors

Languages