PeopleofSuperintelligence

Researcher

Jeremy Avigad

Jeremy Avigad is a Carnegie Mellon University researcher who works on formal methods and AI for mathematics. After mathematics degrees at Harvard and Berkeley, he joined CMU's Department of Philosophy in 1996. He coauthored Lean's 2015 system description, the ProofNet benchmark for formal mathematics in 2023, and ImProver for optimizing proofs with a language model agent in 2025. His 2022 book, “Mathematical Logic and Computation,” received a 2025 Shoenfield Prize. As of October 2026, he holds the Dean's Chair in Logic and Philosophy of Mathematics and directs the Hoskinson Center for Formal Mathematics and the Institute for Computer-Aided Reasoning in Mathematics.

Works
194
Citations
3,291
h-index
28
Badges

Publication numbers from OpenAlex, as of 27 October 2026.

Timeline

  1. 1989–1996

    Mathematics degrees and Carnegie Mellon

    He earns a BA in mathematics at Harvard College in 1989 and a mathematics PhD at the University of California, Berkeley, in 1995. After a postdoctoral appointment at the University of Michigan in 1995, he joins Carnegie Mellon University's Department of Philosophy in 1996.

  2. 2004

    Checking the prime number theorem

    In 2004, he and students at Carnegie Mellon complete a formally verified proof of the Hadamard–de la Vallée Poussin prime number theorem.

  3. 2015

    The Lean theorem prover

    In 2015, he coauthors “The Lean Theorem Prover (System Description)” with Leonardo de Moura, Soonho Kong, Floris van Doorn and Jakob von Raumer. It describes Lean, an open-source theorem prover under development at Microsoft Research and Carnegie Mellon, designed to support interactive proofs and automated methods.

  4. September 2021

    Hoskinson Center announcement

    In September 2021, Carnegie Mellon announces the Hoskinson Center for Formal Mathematics, with Avigad set to lead it. The center supports Lean's mathematical library, tools for translating mathematical statements into formal language, and educational resources.

  5. 2022

    Mathematical Logic and Computation

    In 2022, Cambridge University Press publishes his book “Mathematical Logic and Computation.” It covers proof theory, model theory, computability and axiomatic foundations, with an emphasis on logic's uses in computer science.

  6. 2023

    ProofNet for undergraduate mathematics

    In 2023, he coauthors ProofNet, a benchmark for automatically translating mathematics into formal language and proving undergraduate mathematics. Its 371 examples pair theorem statements in Lean 3 with statements and proofs in natural language.

  7. 2025

    ImProver for proof optimization

    At the International Conference on Learning Representations in 2025, he coauthors ImProver with Riyaz Ahuja, Prasad Tetali and Sean Welleck. The language model agent rewrites Lean proofs to improve user-defined measures, such as length and declarative structure.

  8. 2025

    A Shoenfield book prize

    In 2025, he receives a Shoenfield Prize from the Association for Symbolic Logic for “Mathematical Logic and Computation.”

  9. August 2025

    Directing ICARM

    In August 2025, he directs the new Institute for Computer-Aided Reasoning in Mathematics at Carnegie Mellon. Supported by the National Science Foundation and the Simons Foundation, the institute brings together AI, formal methods and automated reasoning to support mathematical research.

  10. As of October 2026

    Dean's Chair at Carnegie Mellon

    As of October 2026, he holds the Dean's Chair in Logic and Philosophy of Mathematics in Carnegie Mellon's Department of Philosophy and Department of Mathematical Sciences. He directs the Hoskinson Center for Formal Mathematics and ICARM, and his research focuses on formal methods and AI for mathematics.

Career

  1. NowCarnegie Mellon UniversityDirector, Institute for Computer-Aided Reasoning in Mathematics, Dean’s Chair in Logic and Philosophy of Mathematics
  2. NowAmazonAmazon Scholar
  3. 1996University of MichiganPostdoctoral Researcher

Education

  1. 1995University of California, BerkeleyPhD in mathematics
  2. 1989Harvard UniversityBA in mathematics

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Checked career sources: andrew.cmu.edu.

Colleagues

People named in this biography, and people with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Jeremy Avigad yet. Send us a free-licensed photo.

  1. AMSI-CARMA Lecturer 2015 - Professor Jeremy Avigad - Research and Higher Education rhed.amsi.org.au. Checked 27 October 2026.
  2. Faculty Spotlight: Professor Jeremy Avigad - Department of Philosophy - Dietrich College of Humanities and Social Sciences - Carnegie Mellon University cmu.edu. Checked 27 October 2026.
  3. Jeremy Avigad's Home Page andrew.cmu.edu. Checked 27 October 2026.
  4. The Lean Theorem Prover (System Description) - Microsoft Research microsoft.com. Checked 27 October 2026.
  5. Carnegie Mellon Receives $20 Million to Establish Hoskinson Center for Formal Mathematics in Dietrich College - Dietrich College of Humanities and Social Sciences - Carnegie Mellon University cmu.edu. Checked 27 October 2026.
  6. Mathematical Logic and Computation cambridge.org. Checked 27 October 2026.
  7. [2302.12433] ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics arxiv.org. Checked 27 October 2026.
  8. ImProver: Agent-Based Automated Proof Optimization proceedings.iclr.cc. Checked 27 October 2026.
  9. Shoenfield Prize Recipients – Association for Symbolic Logic aslonline.org. Checked 27 October 2026.
  10. New NSF Institute at CMU Will Help Mathematicians Harness AI and Advance Discoveries - News - Carnegie Mellon University cmu.edu. Checked 27 October 2026.
  11. Jeremy Avigad's Home Page andrew.cmu.edu. Checked 27 October 2026.