Theorem Proving

A proof is a program. A theorem is a type. Once you see that you cannot unsee it, and a lot of what looks like two separate fields turns out to be one field photographed from two sides.

Most people who hear about the Curry-Howard correspondence file it as a curiosity. It is the reason a modern theorem prover is structurally the same shape as a small functional compiler. A tiny trusted core. A handful of axioms. A type checker doing arithmetic on propositions. Everything else is sugar on top.

The series builds the idea four ways:

  1. Propositions are types. What Curry-Howard actually says, and why it changes how you read both programs and proofs.
  2. A tiny prover in Python. A term language, a checker, and a trusted kernel, written explicitly so the architecture is impossible to hide.
  3. A mini-Lean in Julia. Guillermo Angeris fits a working prover into 61 lines of Julia by leaning on the type system. Six axioms, and the compiler does the rest.
  4. Writing proofs in Lean. The same three theorems from the Python prover, now in Lean 4. The version you actually use.

Curry and Howard noticed the pattern. Martin-Löf built a logic out of it. Lean is where it lives now. Start at the top if you want the idea first; start at episode two if you would rather watch the construction and let the idea fall out of it.

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. Here is the 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!