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. There is a headshot here.
I apologize that I can't respond to most requests for advice on research, projects, and manuscripts, or provide arXiv endorsements. 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 prior 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
I direct the Institute for Computer-Aided Reasoning in Mathematics (ICARM). Please check out our web pages, sign up for our mailing list, and consider proposing a workshop, collaborative visit, or summer school.
Prompted by advances in AI over the last few months, I have written an essay, What is mathematics now, and what should it be?
"The problem is the problem: Toward scalable mathematical discovery" by Zeyu Zheng, Shengtong Zhang, Jeremy Avigad, Prasad Tetali, and Sean Welleck is now online: arXiv.
I serve on the scientific advisory board of Palomar, a new registry for formally checked mathematics.
I have been awarded a Shoenfield Prize by the Association for Symbolic Logic for my book, Mathematical Logic and Computation. In the acknowledgments to that book, I noted the influence of Shoenfield's textbook, Mathematical Logic, which was originally published in 1967.
I have written a preface to a story by Simone Severini.
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.
I serve on the Admin Team of the Lean Community and on the board of directors of the Lean Focused Research Organization. I also serve on the advisory board of the new Zulip Foundation.
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.