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.
Mathematical logic, formal methods in mathematics, history and philosophy of mathematics.
Office: Baker Hall 139A
E-mail: avigad@cmu.edu
Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213
My book, Mathematical Logic and Computation, has been published! You can order it on Amazon or find it online. (It may be available in PDF through your university library.) It has already received a kind review from Peter Smith.
Alexander Bentkamp, Ramon Fernández Mir, and I have written a paper on our project to carry out verified convex optimization with Lean 4.
I have been working on verification of blockchain applications with colleagues at StarkWare. We have recently 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.
I recently gave a talk, Varieties of mathematical understanding, at the Fields Institute. I gave another talk, The digital revolution in mathematics, at the Microsoft Research Summit 2022. The slides for both can be found under Talks.
Erika Abraham, Kevin Buzzard, Jordan Ellenberg, Timothy Gowers, Marijn Heule, and Terence Tao and I are organizing an IPAM workshop on machine assisted proofs, which will be held February 13-17, 2023.
Heather Macbeth, Patrick Massot, and I are organizing a summer school on the formalization of mathematics, which will be held at MSRI June 5-16, 2023.
Stephen Mackereth and I have written a paper, Two-sorted Frege arithmetic is not conservative, that will appear in the Review of Symbolic Logic.
I have written an essay on the role of syntax and semantics in philosophy of mathematics in the style of a short story by Raymond Carver.
Seul Baek, Alex Bentkamp, Marijn Heule, Wojciech Nawrocki, and I discovered an inconsistency in a logic puzzle by Raymond Smullyan: arXiv. It will be published in the American Mathematical Monthly.
Kevin Buzzard, Robert Lewis, Patrick Massot, and I have been writing an online textbook, Mathematics in Lean (with associated repository here).
Marijn Heule and I are teaching a course Logic and Mechanized Reasoning. You can see the course page, the textbook (still a work in progress), a PDF version of the textbook, and the course repository. You can also see the slides and video from an associated talk.
Good news from some past students: Robert Y. Lewis joined the Department of Computer Science at Brown University, Floris van Doorn started a postdoctoral position in Paris. Paula Neeley is now an R&D Engineer in the Formality Group at Synopsis. Jason Rute is now a postdoctoral researcher in Mathematics of AI at IBM. Cayden Codel is starting the PhD program in CS and Minsung Cho is starting the PhD in CS at Northwestern. Mario Carneiro has defended his dissertation.
I am on the editorial boards of the Journal of Automated Reasoning and Logical Methods in Computer Science.