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, a research center at Carnegie Mellon, and I hold a Dean's Chair in Logic and Philosophy of Mathematics. 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.
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 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.
ICARM is looking to hire up to three innovation engineers. Feel free to contact me with questions.
I have written a draft of a chapter on mathematical understanding.
I recently 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.
Thomas Zhu, Joshua Clune, Albert Jiang, Sean Welleck, and I have made available a prototype sledgehammer for Lean. You can read about the sledgehammer and our method of premise selection here.
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 do formal verification for StarkWare, a company that provides efficient means of establishing computational claims on blockchain. You can see some of our results online, and you can find more information under Papers and Talks.
I serve on the Admin 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.
If you are thinking of applying to graduate school, here is some general information and advice.