I am a PhD student at the University of Pittsburgh, under the supervision of Tom Hales.
My research interests are in formal verification, in particular formal proofs and the applications of machine learning to automated theorem proving.
I am currently working on a formalization of the independence of the continuum hypothesis.
Papers, preprints, and notes
A formalization of forcing and the unprovability of the continuum hypothesis (joint w/Floris van Doorn). Draft submitted to ITP 2019.
Here is my MSc. thesis.
Here are some notes on theories, interpretations, and pretoposes, meant as a revised version of Chapter 1 of my master's thesis.
Here is a brief introduction to sheaf cohomology that I wrote for a course project.
Here are (what started as) notes for my talk at the Harvard logic seminar on 6 February 2018.
Here are notes I helped write on Kevin Buzzard's course at the MSRI on automorphic forms and the Langlands program.
Here are some (incomplete) notes I made in summer 2016 on internal covers and internal categories in Def(T); among other things, I work out a general adjoint functor theorem for internal anafunctors.
With Tom Hales, I am organizing the Hanoi Lean 2019 workshop.
Here are (updated) slides for a talk on strong conceptual completeness for Boolean coherent toposes which I gave at the McGill logic, category theory, and computation seminar on 5 December 2017.
Here are slides for a talk on strong conceptual completeness for Boolean coherent toposes which I gave at the CT Octoberfest 2017 at CMU on 28 October, 2017.
Here are slides for a talk on strong conceptual completeness and internal adjunctions in Def(T) which I gave at the McMaster University model theory seminar on 3 October, 2017.
Here is a poster on an ultraproduct definability criterion for omega-categorical theories which I presented at the 2017 model theory meetings in Wrocław and Będlewo.
Here are some slides for a talk on reconstruction problems for first-order theories (and other things I'm working on for my master's thesis) at the 2017 GSCL at UIUC.
Here are some slides for an expository talk on model-theoretic Galois theory that I gave at the 2016 GSCL at Notre Dame.
I keep a blog at: Eat. Sleep. Math.
I contribute (and welcome improvements) to model theory articles on the nLab: