Research
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 cubeandconquer 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

Learning cubing heuristics for SAT from DRAT proofs. Accepted to AITP 2020.

A formal proof of the independence of the continuum hypothesis. Joint with Floris van Doorn. Accepted to CPP 2020.

A formalization of forcing and the unprovability of the continuum hypothesis. Joint with Floris van Doorn. Accepted to ITP 2019.

Reconstruction problems for firstorder theories (master’s thesis)
Talks and conferences

A formal proof of the independence of the continuum hypothesis. (Talk at CPP 2020).

A formal proof of the independence of the continuum hypothesis. (Talk at Lean Together 2020).

A formalization of forcing and the unprovability of the continuum hypothesis. (Talk at ITP 2019).

I coorganized the Hanoi Lean 2019 workshop. Exercises and slides are available here.

Strong conceptual completeness for ℵ₀categorical theories (notes for Feb. 2018 talk at Harvard Logic seminar)

Strong conceptual completeness for Boolean coherent toposes (slides for talks given at McGill, CMU, CUNY, UMCP)

Ultraproduct definability criteria for ωcategorical theories (poster for 2017 model theory meetings in Wrocław and Będlewo)

Modeltheoretic Galois theory (slides for an expository talk at the 2016 GSCL at Notre Dame)
Notes

Theories, interpretations, and pretoposes (an introduction to firstorder categorical logic, meant as a revised version of Chapter 1 of my master’s thesis)

Automorphic forms and the Langland’s program (notes I helped write on Kevin Buzzard’s 2017 course at the MSRI)

Definable categories (research from 2016 on internal covers and categories internal to Def (T), including a general adjoint functor for internal anafunctors)