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

Robert Lewis I and organized a meeting, Formal Methods in Mathematics / Lean Together 2020.

Lean's mathlib community has written an overview of the library: arXiv. It has been accepted to

Certified Proofs and Programs (CPP) 2020.The project page is here and the github repository is here.My paper on the reliability of mathematical inference has been accepted to

Synthese:doi. There is a preprint here: philsci archive.I am honored to have been interviewed by Richard Marshall in his 3:16 series, and also to have been interviewed by the

High School Journal of Mathematics, an online journal staffed entirely by high school students.Kevin Buzzard has given an inspiring talk on interactive theorem proving: slides, video.

My article, "The mechanization of mathematics," has been reprinted in the Best Writing on Mathematics in 2019.

I recently gave a talk on automated reasoning for mathematics: pdf. Here is a repository I set up to gather data: github.

An article I wrote on the relationship between philosophy and mathematics, with some reflection on the state of the philosophy of mathematics today, has appeared in Aeon: html.

I have contributed to the development of a new theorem prover, Lean, and its library. There is a tutorial introduction here: online version, pdf. You can meet the Lean community on a Zulip channel.

Rob Lewis, Floris van Doorn, and I have prepared materials based on Lean for an undergraduate introduction to logic and mathematical proof: online version, pdf. You can read about the course here: pdf. I also maintain a web page with additional resources for using formal methods in education.

I am on the editorial boards of the

Journal of Automated ReasoningandLogical Methods in Computer Science.