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

Research Interests

Mathematical logic, proof theory, philosophy of mathematics, formal verification, automated reasoning, history of mathematics.


Office: Baker Hall 135E
Phone: (412)268-8149

Postal Address

Department of Philosophy
Baker Hall 161
Carnegie Mellon University
Pittsburgh, PA 15213


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.

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 teaching a new course, Logic and Mechanized Reasoning, in the fall of 2021. You can see the course page, the textbook (still a work in progress), a PDF version of the textbook, and the course repository.

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.

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:

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 Reasoning and Logical Methods in Computer Science.