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. I am now working on a few open source projects, with more details to come soon!

Education

I grew up in Fort Wayne, Indiana, and was interested in mathematics, computer science, and artificial intelligence as a child. When in high school, I took courses concurrently at Purdue University, Fort Wayne. I dropped out half-way through my sophomore year to attend Indiana University, where I completed my bachelor's and master's degrees in pure mathematics. While there, I was interested in the Langlands program, and I wanted to become a mathematics professor.

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.