About

I work at the intersection of automated theorem proving, autoformalization, and software verification. This means that I take things which are fuzzy and informal—like handwritten mathematics or logic in software—and convert them into code (e.g., Lean 4) that can be compiled and checked for correctness.

I work at Project Numina, where I led the development of Fuse. I organize NYC Lean. I have worked on projects like LeanExplore, and was previously at the company Axiom.

Why AI for mathematics?

My original interest was in automating mathematics research after seeing how Alexander Grothendieck and Jacob Lurie constructed large mathematical theories. I think that the limiting factor of a lot of research is the breadth and pace at which humans can work. Having machines that can simultaneously understand all of the literature and work industriously seems ripe for an "AlphaGo" moment. It looks like this is happening as of late 2026!