Writing
Mostly math & CS. Occasionally food, occasionally miles.
- Formalizing R(3,3)=6 in Rocq
Machine-verified proof of the friends and strangers theorem using computational brute force in Rocq.
- ZX-Calculus: Rewriting Your Way to Smaller Circuits
ZX-calculus turns quantum circuits into flexible graphs. Simple rewrite rules yield provably equivalent - often smaller - circuits.
- Buzen's Algorithm
12 billion states reduced to 500 operations. How a 1973 algorithm makes closed queueing networks tractable.
- Goodstein Sequences
A simple arithmetic process that grows faster than any computable function, yet always terminates - and this fact is unprovable in standard arithmetic.
- Quantum Counterfeit Coins
A quantum algorithm for the counterfeit coin problem using Bernstein-Vazirani, achieving O(1) query complexity vs classical O(log N).