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 has just been announced. These slides provide an overview of the institute and its goals, and you can see me talk about it in a short news segment on a local TV station in Pittsburgh.
I participated in the writing of a community whitepaper, The future of artificial intelligence and the mathematical and physical sciences (AI+MPS).
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 recently gave the Tarski Lectures in Berkeley. You can find the slides under Talks.
I have written an essay, Is mathematics obsolete?, on the importance of mathematics and symbolic reasoning in the age of AI.
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 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.
If you are thinking of applying to gradaute school, here is some general information and advice.