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 and I are organizing a meeting, Formal Methods in Mathematics / Lean Together 2020. It will take place January 6-10, 2020.

I have written a draft of a paper on the reliability of mathematical inference: philsci archive.

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

An article on a method of constructing data types as quotients of polynomial functors, with Mario Carneiro and Simon Hudon, has been accepted to ITP 2019: pdf.

An article on computability-theoretic aspects of conditional independences, written with Nathanael L. Ackerman, Cameron E. Freer, Daniel M. Roy, and Jason M. Rute, was presented at LICS 2019: pdf

Joseph Quinsey's 1980 PhD thesis,

Some problems in logic: Applications of Kripke's notion of fulfilment, has been re-typeset and can now be found on arXiv.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. 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 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 Reasoning,Computability,Logical Methods in Computer Science, theJournal of Logic and Analysis, and theJournal of Formalized Reasoning. The last three are open access journals.