I work at Google as a software engineer in machine learning. Outside work I do mathematics, mostly old open problems like whether planets can spin together as one in infinitely many ways, or how few multiplications it takes to multiply two 3×3 matrices. A computer does the searches and calculations that are too big to do by hand. Where I can, Lean checks the whole proof, including the computer’s part. I also write essays on Substack, on things like why tech doesn’t grow in New York the way it does in SF Bay and Seattle.
Matrix multiplicationHow few multiplications does a 3×3 matrix product need?+Laderman’s 23
GenomicsWhat do genome benchmarks measure?+Operon prediction and benchmark audits
Sorting networksHow few comparators sort 13 numbers?+Bose and Nelson’s question at 13 inputs
Quantum error correctionHow much noise can the surface code take?+Proven lower bounds on thresholds
EntanglementWhich entangled states can be distilled?+Werner states and PPT²
Lattice modelsConfinement and percolation on lattices+Polyakov’s mechanism, Aizenman–Grimmett
Verified computingHow do you check what a computer did?+Lean’s kernel and COBOL translations
WritingWho pays the line cook+Substack, October 2026