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 hold a Dean's Chair in Logic and Philosophy of Mathematics. You can read my CV, see a picture of me, or see another one.
Research Interests
Formal methods and AI for mathematics, mathematical logic, 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
I am giving the Tarski Lectures in Berkeley. You can find the slides under Talks.
I have written an essay, Is mathematics obsolete?, on the importance of mathematics and symbolic reasoning in the age of AI.
In November, I gave a talk, You Want Proof? I'll Give You Proof! Mathematical Arguments from Euclid to Lean at the National Museum of Mathematics in New York City.
Ursula Martin, Heather Macbeth, Patrick Massot, Natarajan Shankar, and I are organizing a workshop, Big Proof: Formalizing Mathematics at Scale, at the Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, June 9-13, 2025.
Marijn Heule, María Inés de Frutos-Fernández, Floris van Doorn, Adam Wagner, and I organized a workshop, AI for Mathematics and Theoretical Computer Science, at the Simons-Laufer Mathematical Science Institute and the Simons Institute for Theoretical Computer Science, Berkeley, April 7-11, 2025.
My book, Mathematical Logic and Computation, has been published. You can read the preface and table of contents, and you can order it on Amazon or find it online. A PDF version may be available through your university library.
I have been working on verification of blockchain applications with colleagues at StarkWare, and some of our work is publicly available.
I serve on the Admin Team and the Code of Conduct Team of the Lean Community, and I serve on the board of directors of the Lean Focused Research Organization.
I serve on the scientific advisory board of the new Annals of Formalized Mathematics. I am on the editorial boards of the Journal of Automated Reasoning and the Journal of Symbolic Logic. For the types of JSL papers I will handle, see here.