I’m a software engineer (ML) at Google and an independent researcher in mathematics, working on open problems, mostly with computer-assisted proofs. One result is that, for every choice of five positive masses, there are finitely many planar central configurations up to similarity, which settles Smale’s sixth problem for five bodies in the plane (Albouy and Kaloshin had proved this for almost all masses). Another is that the rank of 3×3 matrix multiplication over F2 is 23, so no bilinear algorithm for 3×3 matrices over F2 uses fewer than Laderman’s 23 multiplications. Both results are in preprints, and the main theorem of each is proved in the Lean proof assistant and checked by Lean’s kernel.
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 proven threshold of at least 2×10−3 for matching on the rotated surface code under circuit-level noise+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 2Fork of a bracket colorizer for VS Code+160k+ installs
WritingWho pays the line cook+Substack, October 2026