-
Theorem Proving
Writing Your First Proofs in Lean
The same three theorems from the Python prover, now in Lean 4.
-
Theorem Proving
Programming a Mini-Lean in Julia’s Type System
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.
-
Theorem Proving
Building a Tiny Theorem Prover in Python
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.
-
Theorem Proving
Propositions Are Types, Proofs Are Programs
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.