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.
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.