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, and confinement in lattice gauge theory. Most of the proofs are computer-assisted, and twenty-two are formalized in Lean, with five 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 at least 44 comparators+Computer search
Lattice gauge theoryConfinement at every coupling in 3D U(1)+Comparison with the Villain action
Celestial mechanicsUniqueness of convex four-body central configurations+Interval arithmetic, Lean 4
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