Faculty Spotlight: Professor Jeremy Avigad

When he was a graduate student, Professor Jeremy Avigad didn’t expect to find himself in a Philosophy Department. Now, nearly 22 years after coming to Carnegie Mellon, he can’t imagine being anywhere else.

“This department is a natural home for me,” Avigad explains. “What makes logic and the foundations of mathematics so fascinating is that it brings together mathematics, philosophy, computer science, and linguistics, in an interesting and meaningful way. I am grateful to be in a department that can bring all these disciplines together under one roof.”

Avigad earned his undergraduate degree in mathematics at Harvard, and then went on to earn his Ph.D. in the same discipline at the University of California at Berkeley.  Although he took a few philosophy courses as an undergraduate, he likes to say that his first real courses in philosophy were the ones that he taught here.

“As an undergraduate, I took a philosophy course on Gödel’s incompleteness theorems, and as a graduate student, I sat in on a course on the notion of logical consequence. But I also did a lot of reading on my own,” he says. “I have always been interested in the history and philosophy of mathematics. I have been reading about logic and foundations since I was in high school.”

Coming to Carnegie Mellon was serendipitous for Professor Avigad. After completing his Ph.D. in 1995, he secured a three-year post-doctoral appointment at the University of Michigan. During his first semester there, the Department of Philosophy at CMU advertised for a logician.

“I visited the University of Wisconsin to give a talk, and someone I knew there told me about the job and said that I should apply for it,” Avigad says. “And I remember saying, ‘Yeah, but it’s a philosophy department!’” He told me that they liked mathematicians here, so I took a chance and rushed to get an application together.” He was hired, and started the following year, in 1996.

Since he has been here, Professor Avigad has worked, broadly speaking, on understanding mathematical reasoning and how it works. He approaches this subject from multiple perspectives, all rooted in logic.

“I have worked on applications of logic to mathematics itself, and I have also used logic to understand how mathematics has evolved throughout its history,” he explains. “Why do we practice mathematics the way we do? Mathematicians have an idiosyncratic way of speaking, and the history of the subject is a valuable tool for understanding why we adopt such language. I get to ask why we reason about numbers, sets, and functions the way we do.”

Another longstanding interest of Professor Avigad’s involves a computational side of mathematics, namely, using computers to carry out mathematical proofs and to verify that there are no mistakes. That work is part of a branch of computer science known as “formal verification,” in which logical tools and methods are used to verify correctness.

“In computer science, such methods are used to verify hardware and software, to guarantee that a system does what it was designed to do. The same technology can be used to verify mathematical reasoning,” he explains. “I have been involved in the development of interactive proof assistants, which are computer systems that work with a user interactively to develop and check mathematical proofs.”

“In the last few years I have been involved with a project led by Leonardo de Moura, a colleague at Microsoft Research,” he continues, “developing a new theorem prover called Lean. A number of students in our department have been involved. It is nice to work with such bright, talented people, and it’s exciting to know that we are witnessing the early days of a technology that is going to transform mathematics in the years to come.”

Professor Avigad has spent two summers as a Visiting Researcher at Microsoft. Although Lean was not designed as an educational tool, he has been using it in course he taught this fall, Logic & Mathematical Inquiry, and he has found it to be useful in teaching undergraduates how to reason mathematically.

In the summer of 2017, Avigad was an organizer of a six-week program at the Isaac Newton Institute for Mathematical Sciences in Cambridge, England. The program was called “Big Proof,” and focused on theorem proving technology.

“The workshop was exciting because the participants shared the sense that we are working on something new and vitally important. It was gratifying to be a part of the organizing committee and see it turn out so well, bringing people together from all over the world,” he says.

In the spring, Professor Avigad will be teaching a Dietrich College freshman seminar on the history and philosophy of mathematics. He has enjoyed teaching it in the past, and looks forward to teaching it again.

Among his other expository contributions, he has led the development of online documentation for Lean, and, with graduate students Robert Lewis and Floris van Doorn, has written an interactive online textbook, Logic and Proof, to accompany Logic and Inquiry. He is also working on a textbook, Mathematical Logic, which he hopes will provide a helpful resource to students and newcomers to the field.