Jesse Michael Han

   Research      Blog      Misc.   


I am a mathematics PhD student at the University of Pittsburgh, under the supervision of Tom Hales.

I received my BSc from UCLA in 2015, and my MSc from McMaster University in 2018. My background is in model theory and categorical logic.


My research is at the intersection of formal proofs, automated reasoning, and machine learning.

Recently, I worked on applying large language models for theorem proving in Lean, and on a solver for IMO geometry problems.

Before that, I led the Flypitch project.


E-mail: jessemichaelhan [at] gmail [dot] com