Jeremy Avigad
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
24
Venues
10
Active years
2001–2026
Best venue rank
A*
Where they publish
Papers
24 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | ITP | An End-To-End Verification of Keller's Conjecture. | James Gallicchio, Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2026 | ITP | LeanArchitect: Automating Blueprint Generation for Humans and AI. | Thomas Zhu, Pietro Monticone, Sean Welleck, Jeremy Avigad |
| 2026 | TACAS | Hint-Based SMT Proof Reconstruction. | Joshua Clune, Haniel Barbosa, Jeremy Avigad |
| 2025 | CAV | Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. | Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad |
| 2025 | ICLR | ImProver: Agent-Based Automated Proof Optimization. | Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck |
| 2025 | ITP | Canonical for Automated Theorem Proving in Lean. | Chase Norman, Jeremy Avigad |
| 2024 | FMCAD | Verified Substitution Redundancy Checking. | Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2024 | IJCAR | Automated Reasoning for Mathematics. | Jeremy Avigad |
| 2024 | ITP | Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. | Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad |
| 2023 | FMCAD | Verified Encodings for SAT Solvers. | Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule |
| 2023 | ITP | A Proof-Producing Compiler for Blockchain Applications. | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2023 | SAT | Certified Knowledge Compilation with Application to Verified Model Counting. | Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule |
| 2023 | TACAS | Verified reductions for optimization. | Alexander Bentkamp, Ramon Fernndez Mir, Jeremy Avigad |
| 2022 | CPP | A verified algebraic representation of cairo program execution. | Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman |
| 2019 | ITP | Data Types as Quotients of Polynomial Functors. | Jeremy Avigad, Mario Carneiro, Simon Hudon |
| 2019 | LICS | Algorithmic barriers to representing conditional independence. | Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute |
| 2018 | ITP | Erratum to: Interactive Theorem Proving. | Jeremy Avigad, Assia Mahboubi |
| 2015 | CADE | The Lean Theorem Prover (System Description). | Leonardo Mendona de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer |
| 2014 | ITP | A Heuristic Prover for Real Inequalities. | Jeremy Avigad, Robert Y. Lewis, Cody Roux |
| 2013 | ITP | A Machine-Checked Proof of the Odd Order Theorem. | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Franois Garillot, Stphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Thry |
| 2012 | CADE | δ-Complete Decision Procedures for Satisfiability over the Reals. | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
| 2012 | LICS | Delta-Decidability over the Reals. | Sicun Gao, Jeremy Avigad, Edmund M. Clarke |
| 2004 | CADE | Formalizing O Notation in Isabelle/HOL. | Jeremy Avigad, Kevin Donnelly |
| 2001 | LICS | Eliminating Definitions and Skolem Functions in First-Order Logic. | Jeremy Avigad |