Theorem Proving

A four-part series on the connection between types and proofs: the Curry-Howard correspondence, a tiny prover implemented explicitly in Python, a mini-Lean embedded in Julia’s type system, and writing proofs in Lean.

Episodes

Propositions Are Types, Proofs Are Programs Episode 1 – Propositions Are Types, Proofs Are Programs
12 min read Keywords:  curry-howard, type theory, theorem proving, logic, formal verification

The Curry-Howard correspondence says that types and logical propositions are the same thing. Understanding why changes how you think about both programming and mathematics.

Building a Tiny Theorem Prover in Python Episode 2 – Building a Tiny Theorem Prover in Python
7 min read Keywords:  theorem proving, python, type theory, formal verification, logic, curry-howard

A tiny theorem prover is just a term language, a checker, and a small trusted kernel. We build one in plain Python to make the architecture explicit.

Programming a Mini-Lean in Julia's Type System Episode 3 – Programming a Mini-Lean in Julia’s Type System
18 min read Keywords:  theorem proving, julia, lean, curry-howard, Type Systems, formal verification

Guillermo Angeris builds a working theorem prover in 61 lines of Julia. A tiny trusted kernel, six axioms, and the compiler does the rest. This article walks through the full construction.

Writing Your First Proofs in Lean Episode 4 – Writing Your First Proofs in Lean
7 min read Keywords:  lean, theorem proving, formal verification, tactics, induction, lean 4

The same three theorems from the Python prover, now in Lean 4.

This series is complete!