Welcome to my home page. I am a professor in the Department of Philosophy and the Department of Mathematical Sciences at Carnegie Mellon University, and associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can also read my CV.
Mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning, history of mathematics.
Baker Hall 135E
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
I will be giving a talk in a special session, "Mathematical Information in the Digital Age of Science," at the Joint Mathematical Meetings in San Diego in January, 2018.
"Modularity in Mathematics" has been accepted to the Review of Symbolic Logic. Preprint: pdf.
I was a co-organizer of the Big Proof program at the Isaac Newton Institute in Cambridge, England. Most of the talks and seminars were recorded and are available online.
I have started maintaining a web page listing resources for using formal methods in education.
Minchao Wu has successfully defended his MS thesis: A formally verified proof of Kruskal's tree theorem in Lean, pdf.
I am on the editorial boards of the Journal of Automated Reasoning, Computability, Logical Methods in Computer Science, the Journal of Logic and Analysis, and the Journal of Formalized Reasoning. The last three are open access journals.
I am contributing to the development of a new theorem prover, Lean. There is a tutorial introduction here: online version, pdf.
Rob Lewis, Floris van Doorn, and I have prepared materials based on Lean for an undergraduate introduction to logic and mathematical proof: online version, pdf.