Research

I am interested both in formalization and the development of tools for interactive theorem proving. I have contributed to the Lean mathematical library. Some of these commits come from the formalization I have done in the course of my Master’s studies.

I have also worked on verification of optimized decision procedures of modal logics in Lean. As a researcher I believe that the sacrifice of efficiency for trustworthiness can be kept relatively low in future.

With Robert Lewis, I developed an interface between Lean and the computer algebra system (CAS) Mathematica. The link we have developed is generic, extensible, and can be used for communication in both directions. Here is a detailed description of this project.

On the other hand, I am interested in applying machine learning to improving automation in interactive theorem proving. I have been developing an interface that enables querying the interactive theorem prover HOL4 from within Python, and thus opens the possibility to treat HOL4 as an envrionment for reinforcement learning. See our poster TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning at MATH-AI 2021 for a short summary.

Talks / Slides