Welcome to my home page. I am a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University. I am the director of the Hoskinson Center for Formal Mathematics, and I am associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can read my CV.
Mathematical logic, formal methods in mathematics, history and philosophy of mathematics.
Office: Baker Hall 135E
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
I was featured in an article in the New York Times on interactive theorem proving, automated reasoning, and machine learning for mathematics.
Patrick Massot and I have recently ported Mathematics in Lean to Lean 4. It is still a work in progress.
I have been working on verification of blockchain applications with colleagues at StarkWare. We have made public a proof-producing version of their compiler for the Cairo language, as well as a verification of code used to validate cryptographic signatures. The paper has been accepted to Interactive Theorem Proving (ITP) 2023.
You can find other activities and events listed on the Hoskinson Center web pages.
I serve on the board of directors of the Lean Focused Research Organization.
I am on the editorial boards of the Journal of Automated Reasoning and Logical Methods in Computer Science.