I received my Ph.D. from Carnegie Mellon University in 2018. I am interested in formal theorem proving and homotopy type theory. Formal theorem proving involves building a formal library of mathematics where each proof can be automatically checked by a computer program. I am a maintainer the library mathlib (https://leanprover-community.github.io/). Homotopy type theory is a new research area that investigates a connection between geometry and logic.