About

I am a pure mathematician by training, now working 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 Lean 4 code, that can be compiled and checked for correctness. 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.