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
The Lean Theorem Prover (System Description), by Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer, has been awarded the CADE-25 Skolem Award.
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 PhD student, Chase Norman, has released the first version of Canonical, a search procedure for dependent type theory with an associated Lean tactic. You can read about it here. The paper has been accepted to Interactive Theorem Proving (ITP).
I recently gave the Tarski Lectures in Berkeley. You can find the slides under Talks.
Marijn Heule, María Inés de Frutos-Fernández, Floris van Doorn, Adam Wagner, and I recently 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.
I have written an essay, Is mathematics obsolete?, on the importance of mathematics and symbolic reasoning in the age of AI.
Last 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.
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.