Projects

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.

github.com/corun1024/4ct

Tummy Checker

A web app that asks you to put your phone on your stomach, then tells you how full it is.

tummyscan.xyz