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.
Research Interests
Mathematical logic, formal methods in mathematics, history and philosophy of mathematics.
Contact
Office: Baker Hall 135E
E-mail: avigad@cmu.edu
Postal Address
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
Announcements
My book, Mathematical Logic and Computation, has been published. You can order it on Amazon or find it online. A PDF version may be available through your university library.
I was featured in an article in the New York Times on interactive theorem proving, automated reasoning, and machine learning for mathematics.
I recently gave a talk, Is mathematics obsolete? at the Santa Fe Institute. You can find the slides under Talks.
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.