About

Jeremy Avigad is a professor with a significant role in graduate education, having served as the Director of Graduate Studies in Philosophy at Carnegie Mellon University from 2005 to 2009 and again from 2011 to 2012. His academic work involves mentoring PhD and MS students across various disciplines including Mathematical Sciences, Computer Science, Logic, Computation, and Methodology. Avigad's students have worked on topics such as formal verification, proof assistants, computable analysis, and formalization of mathematical theories, reflecting his engagement with the intersection of logic, mathematics, and computer science. He has also supervised postdoctoral researchers and served on numerous PhD and MS committees, indicating a broad influence in shaping research in logic, computation, and related fields. Avigad's leadership extended to directing the Department of Philosophy's major in Logic and Computation from 1997 to 2005, highlighting his commitment to interdisciplinary education and research at the nexus of philosophy, logic, and computer science.

Research topics

• Computer Science
• Philosophy
• Epistemology
• Sociology
• Mathematics
• Economics
• Artificial Intelligence
• Engineering
• Arithmetic
• Programming language
• Management science
• Engineering ethics
• Mathematical economics

Selected publications

• Hint-Based SMT Proof Reconstruction

  Lecture notes in computer science · 2026-01-01

  book-chapterSenior author
  PublisherDOI

• Anatomy of a Formal Proof

  Notices of the American Mathematical Society · 2025-01-10 · 1 citations

  articleOpen access1st authorCorresponding
  PublisherDOI

• A Proof-Producing Compiler for Blockchain Applications

  Journal of Automated Reasoning · 2025-04-11

  articleOpen access1st authorCorresponding

  Abstract CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.

  PublisherOA PDFDOI

• Certified Knowledge Compilation with Application to Formally Verified Model Counting

  ArXiv.org · 2025-01-22

  preprintOpen access

  Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from the decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

  PublisherOA PDFDOI

• Lean-auto: An Interface between Lean 4 and Automated Theorem Provers

  ArXiv.org · 2025-05-20 · 1 citations

  preprintOpen accessSenior author

  Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP's logical system to the ATP's logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4 under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4's math library Mathlib4.

  PublisherOA PDFDOI

• A Proof-Producing Compiler for Blockchain Applications

  ArXiv.org · 2025-01-25

  preprintOpen access1st authorCorresponding

  CairoZero is a programming language for running decentralized applications (dApps) at scale. Programs written in the CairoZero language are compiled to machine code for the Cairo CPU architecture and cryptographic protocols are used to verify the results of execution efficiently on blockchain. We explain how we have extended the CairoZero compiler with tooling that enables users to prove, in the Lean 3 proof assistant, that compiled code satisfies high-level functional specifications. We demonstrate the success of our approach by verifying primitives for computation with the secp256k1 and secp256r1 curves over a large finite field as well as the validation of cryptographic signatures using the former. We also verify a mechanism for simulating a read-write dictionary data structure in a read-only setting. Finally, we reflect on our methodology and discuss some of the benefits of our approach.

  PublisherOA PDFDOI

• Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers

  Lecture notes in computer science · 2025-01-01 · 4 citations

  book-chapterOpen accessSenior author

  Abstract Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide general-purpose proof automation in ITPs such as Coq and Isabelle, leveraging the power of ATPs. An important component of a hammer is the translation algorithm from the ITP’s logical system to the ATP’s logical system. In this paper, we propose a novel translation algorithm for ITPs based on dependent type theory. The algorithm is implemented in Lean 4 under the name Lean-auto. When combined with ATPs, Lean-auto provides general-purpose, ATP-based proof automation in Lean 4 for the first time. Soundness of the main translation procedure is guaranteed, and experimental results suggest that our algorithm is sufficiently complete to automate the proof of many problems that arise in practical uses of Lean 4. We also find that Lean-auto solves more problems than existing tools on Lean 4’s math library Mathlib4.

  PublisherOA PDFDOI

• Certified Knowledge Compilation with Application to Formally Verified Model Counting

  Journal of Artificial Intelligence Research · 2025-03-31

  articleOpen access

  Computing many useful properties of Boolean formulas, such as their weighted or unweighted model count, is intractable on general representations. It can become tractable when formulas are expressed in a special form, such as the decision decomposable negation normal form (decision-DNNF). Knowledge compilation is the process of converting a formula into such a form. Unfortunately existing knowledge compilers provide no guarantee that their output correctly represents the original formula, and therefore they cannot validate a model count, or any other computed value. We present Partitioned-Operation Graphs (POGs), a form that can encode all of the representations used by existing knowledge compilers. We have designed CPOG, a framework that can express proofs of equivalence between a POG and a Boolean formula in conjunctive normal form (CNF). We have developed a program that generates POG representations from decision-DNNF graphs produced by the state-of-the-art knowledge compiler D4, as well as checkable CPOG proofs certifying that the output POGs are equivalent to the input CNF formulas. Our toolchain for generating and verifying POGs scales to all but the largest graphs produced by D4 for formulas from a recent model counting competition. Additionally, we have developed a formally verified CPOG checker and model counter for POGs in the Lean 4 proof assistant. In doing so, we proved the soundness of our proof framework. These programs comprise the first formally verified toolchain for weighted and unweighted model counting.

  PublisherDOI

• Mathematics and the formal turn

  Bulletin of the American Mathematical Society · 2024-02-15 · 13 citations

  articleOpen access1st authorCorresponding

  Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. This article enumerates some of the ways that these and related technologies can help us do mathematics.

  PublisherOA PDFDOI

• Anatomy of a Formal Proof

  arXiv (Cornell University) · 2024-11-05

  preprintOpen access1st authorCorresponding

  Interactive proof assistants make it possible for ordinary mathematicians to write definitions and theorems in a formal proof language, like a programming language, so that a computer can parse them and check them against the rules of a formal axiomatic foundation. This article describes the experience of working with a proof assistant and considers the impact the technology will have on mathematics.

  PublisherOA PDFDOI

Recent grants

• collaborative research: theoretical support for mechanized proof assistants

  NSF · $99k · 2004–2007

• Proof Mining and Formal Verification

  NSF · $232k · 2011–2015

• Verified Computation and Proof

  NSF · $150k · 2016–2018

• Collaborative research: logical support for formal verification

  NSF · $218k · 2007–2010

Frequent coauthors

• Henry Towsner

  California University of Pennsylvania

  7 shared

• K. Donnelly

  Australian National University

  7 shared

• E. ̃Tassi

  6 shared

• Andrea Asperti

  6 shared

• Assia Mahboubi

  Laboratoire des Sciences du Numérique de Nantes

  6 shared

• Cody Roux

  6 shared

• Alexander Bentkamp

  6 shared

• Jason Rute

  6 shared

Labs

• Jeremy Avigad's LabPI