Obfuscated
Projects
Things I've made.
-
The Four Colour Theorem in Lean 4
A complete formal proof: no sorries, no extra axioms, 115,000-odd declarations checked by the Lean kernel. It follows the architecture of Gonthier and Werner's Coq proof, but replaces Coq's kernel VM with certificate checking built on bitwise operations over large naturals, so the kernel can verify all 633 reducible configurations itself.
-
lazylean
A type checker for Lean 4 that reduces terms the way Coq's kernel does. It keeps Lean's type-checking algorithm but replaces substitution with a Krivine machine and call-by-need thunks, so work is shared rather than copied. On proofs that compute, that is worth one to two orders of magnitude in time and memory: it checks the Four Colour Theorem's 201,672-declaration closure in 3.9 core-hours where Lean's kernel needs 7.5, and finishes a reducibility check in 21 GB that exhausts Lean's kernel at 178 GB.
-
Pentumble
A physics platformer: stick, roll and jump your way through a factory. I made it for iOS and Mac in 2013. It runs in the browser now — Claude did the port.
-
Tummy Checker
A web app that asks you to put your phone on your stomach, then tells you how full it is.