Jeremy Avigad

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 Charles C. 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, philosophy of mathematics, formal verification, automated reasoning, history of mathematics.

Office:Baker Hall 135E

Phone:(412)268-8149

E-mail:avigad@cmu.edu

Department of Philosophy

Baker Hall 161

Carnegie Mellon University

Pittsburgh, PA 15213

Cayden Codel has completed his MS thesis, Verified SAT encodings in Lean.

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.

I gave a talk in the Fields Institute MathEd Forum on the use of proof assistants for teaching mathematics, and another one at Learning Mathematics with Lean.

An essay I have written, Varieties of mathematical understanding, has appeared in the

Bulletin of the American Mathematical Society. Doron Zeilberger has criticized it. An essay by Akshay Venkatesh addresses similar themes.Michael Harris has accused me of undertaking a "militant but unsubstantiated attempt to ventriloquize mathematics." The militant attempt is here: preprint, doi.

The Hoskinson Center has been announced! You can read the press release and watch Charles Hoskinson talk about the center on YouTube. You can also watch Charles' presentation and my presentation from the inauguration of the center. The slides that went with my talk are here.

My book,

Mathematical Logic and Computation, will be published by Cambridge University Press. You can read the table of contents and preface: pdf.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.I gave a talk, "Formal mathematics, dependent type theory, and the Topos Institute," in the Topos Institute Colloquium. You can see the slides and the video.

I have been working on verification of blockchain protocols with colleagues at StarkWare. There is a preprint here, a Lean formalization here, and an informal discussion here.

Marijn Heule, Wojciech Nawrocki, and I taught a new 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.I have put online a draft of a chapter on mathematical language, written for the forthcoming

Handbook for the Philosophy of Mathematical Practice.Alexander Bentkamp and I have presented joint work in progress on verified optimization.

I have written a draft of a chapter on logic and foundations for the

Handbook of Proof Assistants and their Applications in Mathematics and Computer Science.Kevin Buzzard, Johan Commelin, Yury Kudryashov, Heather Macbeth, Scott Morrison, and I are co-organizing Lean for the Curious Mathematician, which will be held at ICERM in the summer of 2022.

Heather Macbeth, Patrick Massot, and I are organizing a summer school on the formalization of mathematics, which will be held at MSRI in the summer of 2023.

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.

Kevin Buzzard, Robert Lewis, Patrick Massot, and I have started working on a tutorial, Mathematics in Lean. You can learn about some of the interesting things going on with Lean and mathlib on the Lean community web pages.

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.

An old paper of mine, Forcing in proof theory, has been selected as one of the winners of the

Bulletin of Symbolic Logic's 25th Anniversary Prize.I am on the editorial boards of the

Journal of Automated ReasoningandLogical Methods in Computer Science.