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 am associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can read my CV or see a picture of me.
Research Interests
Mathematical logic, formal methods in mathematics, 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
My book, Mathematical Logic and Computation, has been published. You can read the preface and table of contents, and you can order it on Amazon or find it online. A PDF version may be available through your university library.
Wojciech Nawrocki has completed his MS thesis, User interfaces for computer-assisted mathematics.
The National Academies of Sciences, Engineering, and Medicine has released proceedings of its workshop, Artificial Intelligence to Assist Mathematical Reasoning.
Floris van Doorn is now a professor in the Mathematical Institute of the University of Bonn.
I was featured in an article in the New York Times on interactive theorem proving, automated reasoning, and machine learning for mathematics.
I gave a talk, Is mathematics obsolete? at the Santa Fe Institute. You can find the slides under Talks.
Patrick Massot and I have ported Mathematics in Lean to Lean 4. It is still a work in progress.
I have been working on verification of blockchain applications with colleagues at StarkWare. We have made public a proof-producing version of their compiler for the Cairo language, as well as a verification of code used to validate cryptographic signatures.
You can find other activities and events listed on the Hoskinson Center web pages.
I serve on the board of directors of the Lean Focused Research Organization.
I am on the editorial boards of the Journal of Automated Reasoning and Logical Methods in Computer Science.