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. I go by he/him/his.
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
Johan Commelin, Heather Macbeth, and I have written an article, Anatomy of a Formal Proof, that has just appeared in the Notices of the AMS.
Hannah Fechtner gave a great talk on the formalization of braid groups at Lean Together 2025.
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.
ImProver: Agent-Based Automated Proof Optimization, by Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, and Sean Welleck, has been accepted to ICLR 2025.
Marijn Heule, María Inés de Frutos-Fernández, Floris van Doorn, Adam Wagner, and I are organizing 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.
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.
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.