Projects
-
A formalization of quantum error correction in Lean 4, covering the stabilizer formalism from Pauli groups and the binary symplectic representation up through concrete code families. Includes a machine-checked proof that the L × L toric code is a [[2L², 2, L]] stabilizer code for every L ≥ 2, via formalized homological distance arguments, along with a verification of IBM's [[144, 12, 12]] gross code. Sorry-free.
-
An interactive game that teaches linear algebra by having students prove theorems in Lean. Levels introduce Linear Algebra and the mechanics of machine-checked proof alongside each other.
-
An interactive problem set that teaches abstract algebra through formalization in Lean 4, covering logic-based reasoning, group axioms, homomorphisms, and subgroups. I was one of three project managers for the team of seven that built it at Duke's Math+ 2024.