Jeremy Avigad

Welcome to my home page. I am a professor in the Department of Philosophy at Carnegie Mellon University, and (by courtesy) in the Department of Mathematical Sciences. I am associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can read my CV.

Mathematical logic, proof theory, 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

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.

Marijn Heule and I are launching a new course,

Logic and Mechanized Reasoning, in the fall of 2021.An essay I have written, Varieties of mathematical understanding, will appear in the

Bulletin of the American Mathematical Society.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.Floris van Doorn and I have written a paper on a problem in decentralized control theory.

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 of my recent and current students:

- Robert Y. Lewis will be joining the Department of Computer Science at Brown University in the fall.
- Floris van Doorn will be starting a postdoctoral position in Paris in the fall.
- Mario Carneiro and Seul Baek (with Marijn Heule) have had a paper accepted to TACAS. Wojciech Nawrocki (with Zhenjun Liu, Andreas Fröhlich, Marijn Heule and Armin Biere) has had a paper accepted at SAT.
- Mario's work on Metamath Zero is coming along (see also his YouTube tutorial).
- Seul's work on TESC, a proof format for first-order theorem provers, is coming along. His paper on a formal verifier for it was accepted at ITP.
- Paula Neeley has defended her MS thesis on a formalization of dynamic epistemic logic. She gave a talk about it at Lean Together 2021.
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.