Jesse Michael Han

   Research      Blog      Misc.   


My research interests are in formal verification, in particular formal proofs and the applications of machine learning to automated theorem proving.

I recently worked on on applying the NeuroSAT architecture to the cube-and-conquer paradigm in SAT solving.

With Floris van Doorn, I completed the Flypitch project, producing a formal proof of the independence of the continuum hypothesis in Lean.

With Tom Hales, I developed a parser for Colada, a controlled natural language with semantics in the Calculus of Inductive Constructions. This is part of the Formal Abstracts project.

Papers and preprints

Talks and conferences