Federico Carrone
The open back of a large electromechanical machine: rows of metal rotor drums on the left, and racks of relays laced with red wiring on the right
Series

Theorem Proving

From types and programs to machine-checked proofs

A proof is a program and a theorem is a type. This series builds that idea from Curry-Howard to a tiny Python prover, a mini-Lean in Julia, and real proofs in Lean 4.

On the image The Bombe ran through Enigma settings and threw out every one that contradicted a guessed piece of plaintext. It is an early case of the idea behind this series: reasoning written down precisely enough for a machine to check it. The rebuilt Turing–Welchman Bombe at Bletchley Park, England. Photo: Mike Peel, CC BY-SA 4.0, via Wikimedia Commons.

4 episodes · 44 min in total · Complete

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

  1. Propositions Are Types, Proofs Are Programs

    Propositions Are Types, Proofs Are Programs

    · 12 min read

    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.

  2. Building a Tiny Theorem Prover in Python

    Building a Tiny Theorem Prover in Python

    · 7 min read

    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.

  3. Programming a Mini-Lean in Julia's Type System

    Programming a Mini-Lean in Julia’s Type System

    · 18 min read

    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.

  4. Writing Your First Proofs in Lean

    Writing Your First Proofs in Lean

    · 7 min read

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