Selected publications. My Semantic Scholar profile is much more complete (and up-to-date).

LISA: Language models of ISAbelle proofs

Published in 6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021

We introduce an environment that allows interaction with an Is- abelle server in an incremental manner. With this environment, we mined the Isabelle standard library and the Archive of Formal Proofs (AFP) and extracted 183K lemmas and theorems. We built language models on this large corpus and showed their effectiveness in proving AFP theorems.

Paper link