I’m a software engineer (ML) at Google. Independently, I work on open problems in mathematics: central configurations of the n-body problem, the rank of 3×3 matrix multiplication over F2, sorting networks, quantum error correction, and confinement in lattice gauge theory. Most of the proofs are computer-assisted, and twenty-three are formalized in Lean, with nine more in part or under stated assumptions.
Algebraic complexityThe rank of 3×3 matrix multiplication over F2 is 23+Exact search, Lean 4
Operon FinderOperon prediction for prokaryotic genomes+Deep learning, J. Mol. Biol.
Sorting networks13 inputs need 45 comparators+Computer search, Lean 4
Quantum error correctionA matching threshold of 2×10−3 for the rotated surface code+Exact arithmetic, Lean 4
Lattice gauge theoryConfinement at every coupling in 3D U(1)+Comparison with the Villain action
MarklessInline Markdown rendering in VS Code+47 stars, 4.4k+ installs
Rainbow Brackets 2Bracket colorizer for VS Code+160k+ installs
WritingWho pays the line cook+Substack, October 2026