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, Dean's Chair in Logic and Philosophy of Mathematics, and an Amazon Scholar. I am also the director of the newly-established Institute for Computer-Aided Reasoning in Mathematics, a National Science Foundation mathematical sciences research institute. You can read my CV, see a picture of me, or see another one.
I apologize that I can't respond to most requests for advice on research, projects, and manuscripts. If you are thinking of applying to graduate school, there is some general information and advice here.
Research Interests
Formal methods and AI for mathematics. You can read about my work in mathematical logic, history and philosophy of mathematics, software verification, and history of logic under Research.
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 new Institute for Computer-Aided Reasoning in Mathematics (ICARM) has been launched. Please check out our web pages, sign up for our mailing list, and consider proposing a workshop or summer school.
I am featured in Kevin Hartnett's book, The Proof in the Code, about the development of Lean.
I was recently interviewed by Shannon Shen for the Augmented Mind Podcast. I also served on a VaNTAGe panel with Jennifer Johnson-Leung, Jacob Tsimmerman, and Ravi Vakil to discuss mathematics and AI.
Prompted by recent developments, I have written an essay, Mathematicians in the Age of AI, urging mathematicians to take advances in reasoning technology seriously.
I have written a chapter on mathematical understanding that will appear in the Blackwell Companion to the Philosophy of Mathematics, edited by Alexander Paseau.
I gave the Rademacher Lectures at the University of Pennsylvania, titled "Mathematics in the age of AI." You can find the slides under Talks.
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.
From 2021 to 2026, I carried out formal verification for StarkWare, a company that provides efficient means of establishing computational claims on blockchain. You can read about some of our projects in this blog post or in this public repository, and you can find more information under Papers and Talks.
I serve on the Admin Team of the Lean Community and on the board of directors of the Lean Focused Research Organization.
I serve on the scientific advisory board of the Annals of Formalized Mathematics and on the editorial board of the Journal of Symbolic Logic. For the types of JSL papers I will handle, see here. I also serve on the advisory board of the new Zulip Foundation.