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, and associated with Carnegie Mellon's interdisciplinary program in Pure and Applied Logic. You can also read my CV.

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

Baker Hall 135E

(412)268-8149

avigad@cmu.edu

Department of Philosophy

Baker Hall 161

Carnegie Mellon University

Pittsburgh, PA 15213

USA

I will give a talk on Saint Petersburg, Russia in May,

Mechanization of Mathematics: pdf.I gave a talk in Calgary in March,

Philosophy of Mathematics as a Design Science. You can watch the video."Modularity in Mathematics" has been accepted to the

Review of Symbolic Logic. Preprint: doi, philsci archive.Floris van Doorn has successfully defended his PhD thesis:

On the formalization of higher inductive types and synthetic homotopy theory.Rob Lewis has successfully defended his PhD thesis:

Two tools for formalizing mathematical proofs, pdf.I have contributed to the development of a new theorem prover, Lean. There is a tutorial introduction here: online version, pdf.

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 am on the editorial boards of the

Journal of Automated Reasoning,Computability,Logical Methods in Computer Science, theJournal of Logic and Analysis, and theJournal of Formalized Reasoning. The last three are open access journals.