Jeremy Avigad - RankMe

111 papers A* 4A 4B 12Journal 84Unranked 6

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs. CoRR Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck
2026	—	`conf`	Hint-Based SMT Proof Reconstruction. TACAS (1) Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026	J	`jnl`	Hint-Based SMT Proof Reconstruction. CoRR Joshua Clune, Haniel Barbosa, Jeremy Avigad
2026	J	`jnl`	Implementing Dependent Type Theory Inhabitation and Unification. CoRR Chase Norman, Jeremy Avigad
2026	J	`jnl`	LeanArchitect: Automating Blueprint Generation for Humans and AI. CoRR Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck
2026	J	`jnl`	Mathematicians in the age of AI. CoRR Jeremy Avigad
2025	J	`jnl`	A Proof-Producing Compiler for Blockchain Applications. CoRR Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
2025	J	`jnl`	A Proof-Producing Compiler for Blockchain Applications. J. Autom. Reason. Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
2025	B	`conf`	Canonical for Automated Theorem Proving in Lean. ITP Chase Norman, Jeremy Avigad
2025	J	`jnl`	Canonical for Automated Theorem Proving in Lean. CoRR Chase Norman, Jeremy Avigad
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. CoRR Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	J	`jnl`	Certified Knowledge Compilation with Application to Formally Verified Model Counting. J. Artif. Intell. Res. Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2025	A*	`conf`	ImProver: Agent-Based Automated Proof Optimization. ICLR Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck
2025	J	`jnl`	Is Mathematics Obsolete? CoRR Jeremy Avigad
2025	—	`conf`	Lean-Auto: An Interface Between Lean 4 and Automated Theorem Provers. CAV (3) Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad
2025	J	`jnl`	Lean-auto: An Interface between Lean 4 and Automated Theorem Provers. CoRR Yicheng Qian, Joshua Clune, Clark W. Barrett, Jeremy Avigad
2025	J	`jnl`	Premise Selection for a Lean Hammer. CoRR Thomas Zhu, Joshua Clune, Jeremy Avigad, Albert Qiaochu Jiang, Sean Welleck
2025	J	`jnl`	The Future of Artificial Intelligence and the Mathematical and Physical Sciences (AI+MPS). CoRR Andrew Ferguson, Marisa Lafleur, Lars Ruthotto, Jesse Thaler, Yuan-Sen Ting, Pratyush Tiwary, Soledad Villar, E. Paulo Alves, Jeremy Avigad, Simon Billinge, Camille L. Bilodeau, Keith Brown, Emmanuel J. Candès, Arghya Chattopadhyay, Bingqing Cheng, Jonathan Clausen, Connor W. Coley, Andrew J. Connolly, Fred Daum, Sijia S. Dong, Chrisy Xiyu Du, Cora Dvorkin, Cristiano Fanelli, Eric B. Ford, Luis Manuel Frutos, Nicolás García Trillos, Cecilia Garraffo, Robert Ghrist, Rafael Gómez-Bombarelli, Gianluca Guadagni, Sreelekha Guggilam, Sergei Gukov, Juan B. Gutierrez, Salman Habib, Johannes Hachmann, Boris Hanin, Philip C. Harris, Murray Holland, Elizabeth Holm, Hsin-Yuan Huang, Shih-Chieh Hsu, Nick Jackson, Olexandr Isayev, Heng Ji, Aggelos K. Katsaggelos, Jeremy Kepner, Yannis G. Kevrekidis, Michelle P. Kuchera, J. Nathan Kutz, Branislava Lalic, Ann Lee, Matt LeBlanc, Josiah Lim, Rebecca Lindsey, Yongmin Liu, Peter Y. Lu, Sudhir Malik, Vuk Mandic, Vidya B. Manian, Emeka P. Mazi, Pankaj Mehta, Peter Melchior, Brice Ménard, Jennifer Ngadiuba, Stella Offner, Elsa Olivetti, Shyue Ping Ong, Christopher Rackauckas, Philippe Rigollet, Chad Risko, Philip Romero, Grant M. Rotskoff, Brett Savoie, Uros Seljak, David Shih, Gary Shiu, Dima Shlyakhtenko, Eva Silverstein, Taylor Sparks, Thomas Strohmer, Christopher Stubbs, Stephen Thomas, Suriyanarayanan Vaikuntanathan, René Vidal, Francisco Villaescusa-Navarro, Gregory Voth, Benjamin Wandelt, Rachel Ward, Melanie Weber, Risa Wechsler, Stephen Whitelam, Olaf Wiest, Mike Williams, Zhuoran Yang, Yaroslava G. Yingling, Bin Yu, Shuwen Yue, Ann Zabludoff, Huimin Zhao, Tong Zhang
2024	J	`jnl`	Anatomy of a Formal Proof. CoRR Jeremy Avigad, Johan Commelin, Heather Macbeth, Adam Topaz
2024	—	`conf`	Automated Reasoning for Mathematics. IJCAR (1) Jeremy Avigad
2024	B	`conf`	Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory. ITP Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad
2024	J	`jnl`	ImProver: Agent-Based Automated Proof Optimization. CoRR Riyaz Ahuja, Jeremy Avigad, Prasad Tetali, Sean Welleck
2024	B	`conf`	Verified Substitution Redundancy Checking. FMCAD Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
2023	B	`conf`	A Proof-Producing Compiler for Blockchain Applications. ITP Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
2023	J	`jnl`	An Impossible Asylum. Am. Math. Mon. Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
2023	A	`conf`	Certified Knowledge Compilation with Application to Verified Model Counting. SAT Randal E. Bryant, Wojciech Nawrocki, Jeremy Avigad, Marijn J. H. Heule
2023	J	`jnl`	ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics. CoRR Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, Jeremy Avigad
2023	J	`jnl`	Two-Sorted Frege Arithmetic is not conservative. Rev. Symb. Log. Stephen Mackereth, Jeremy Avigad
2023	B	`conf`	Verified Encodings for SAT Solvers. FMCAD Cayden R. Codel, Jeremy Avigad, Marijn J. H. Heule
2023	—	`conf`	Verified reductions for optimization. TACAS (2) Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
2023	J	`jnl`	Verified reductions for optimization. CoRR Alexander Bentkamp, Ramon Fernández Mir, Jeremy Avigad
2022	B	`conf`	A verified algebraic representation of cairo program execution. CPP Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
2021	J	`jnl`	A verified algebraic representation of Cairo program execution. CoRR Jeremy Avigad, Lior Goldberg, David Levit, Yoav Seginer, Alon Titelman
2021	J	`jnl`	An Impossible Asylum. CoRR Jeremy Avigad, Seulkee Baek, Alexander Bentkamp, Marijn Heule, Wojciech Nawrocki
2021	J	`jnl`	Reliability of mathematical inference. Synth. Jeremy Avigad
2021	—	`conf`	Verified Optimization (work in progress). CICM Workshops Alexander Bentkamp, Jeremy Avigad
2021	J	`jnl`	Verified Optimization. CoRR Alexander Bentkamp, Jeremy Avigad
2020	J	`jnl`	Foundations. CoRR Jeremy Avigad
2020	J	`jnl`	Modularity in Mathematics. Rev. Symb. Log. Jeremy Avigad
2020	J	`jnl`	Preface: Selected Extended Papers from Interactive Theorem Proving 2018. J. Autom. Reason. Jeremy Avigad, Assia Mahboubi
2020	J	`jnl`	Progress on a perimeter surveillance problem. CoRR Jeremy Avigad, Floris van Doorn
2019	A*	`conf`	Algorithmic barriers to representing conditional independence. LICS Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute
2019	B	`conf`	Data Types as Quotients of Polynomial Functors. ITP Jeremy Avigad, Mario Carneiro, Simon Hudon
2018	B	`conf`	Erratum to: Interactive Theorem Proving. ITP Jeremy Avigad, Assia Mahboubi
2018	B	`ed.`	Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings ITP Jeremy Avigad, Assia Mahboubi
2018	J	`jnl`	Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
2018	J	`jnl`	On the computability of graphons. CoRR Nathanael L. Ackerman, Jeremy Avigad, Cameron E. Freer, Daniel M. Roy, Jason M. Rute
2017	J	`jnl`	A Formally Verified Proof of the Central Limit Theorem. J. Autom. Reason. Jeremy Avigad, Johannes Hölzl, Luke Serafin
2017	J	`jnl`	A metaprogramming framework for formal verification. Proc. ACM Program. Lang. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura
2016	J	`jnl`	A Heuristic Prover for Real Inequalities. J. Autom. Reason. Jeremy Avigad, Robert Y. Lewis, Cody Roux
2016	J	`jnl`	Character and Object. Rev. Symb. Log. Jeremy Avigad, Rebecca Lea Morris
2016	B	`ed.`	Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016 CPP Jeremy Avigad, Adam Chlipala
2015	J	`jnl`	Elaboration in Dependent Type Theory. CoRR Leonardo Mendonça de Moura, Jeremy Avigad, Soonho Kong, Cody Roux
2015	J	`jnl`	Homotopy limits in type theory. Math. Struct. Comput. Sci. Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
2015	A	`conf`	The Lean Theorem Prover (System Description). CADE Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer
2014	B	`conf`	A Heuristic Prover for Real Inequalities. ITP Jeremy Avigad, Robert Y. Lewis, Cody Roux
2014	J	`jnl`	A formally verified proof of the Central Limit Theorem. CoRR Jeremy Avigad, Johannes Hölzl, Luke Serafin
2014	J	`jnl`	A heuristic prover for real inequalities. CoRR Jeremy Avigad, Robert Y. Lewis, Cody Roux
2014	—	`ch.`	Computability and analysis: the legacy of Alan Turing. Turing's Legacy Jeremy Avigad, Vasco Brattka
2014	J	`jnl`	Formally verified mathematics. Commun. ACM Jeremy Avigad, John Harrison
2014	J	`jnl`	Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp. Bull. Symb. Log. Jeremy Avigad
2013	B	`conf`	A Machine-Checked Proof of the Odd Order Theorem. ITP Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Théry
2013	J	`jnl`	Homotopy limits in Coq CoRR Jeremy Avigad, Krzysztof Kapulkin, Peter LeFanu Lumsdaine
2013	J	`jnl`	Uniform distribution and algorithmic randomness. J. Symb. Log. Jeremy Avigad
2012	J	`jnl`	A metastable dominated convergence theorem. J. Log. Anal. Jeremy Avigad, Edward T. Dean, Jason M. Rute
2012	J	`jnl`	Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Ann. Pure Appl. Log. Jeremy Avigad, Edward T. Dean, Jason M. Rute
2012	J	`jnl`	Bondy's Theorem. Arch. Formal Proofs Jeremy Avigad, Stefan Hetzl
2012	J	`jnl`	Computability and analysis: the legacy of Alan Turing CoRR Jeremy Avigad, Vasco Brattka
2012	J	`jnl`	Delta-Complete Decision Procedures for Satisfiability over the Reals CoRR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	J	`jnl`	Delta-Decidability over the Reals CoRR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	A*	`conf`	Delta-Decidability over the Reals. LICS Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2012	J	`jnl`	Type Inference in Mathematics. Bull. EATCS Jeremy Avigad
2012	J	`jnl`	Uncomputably Noisy Ergodic Limits. Notre Dame J. Formal Log. Jeremy Avigad
2012	A	`conf`	δ-Complete Decision Procedures for Satisfiability over the Reals. IJCAR Sicun Gao, Jeremy Avigad, Edmund M. Clarke
2011	J	`jnl`	Building a push-button RESOLVE verifier: Progress and challenges. Formal Aspects Comput. Murali Sitaraman, Bruce M. Adcock, Jeremy Avigad, Derek Bronish, Paolo Bucci, David Frazier, Harvey M. Friedman, Heather K. Harton, Wayne D. Heym, Jason Kirschenbaum, Joan Krone, Hampton Smith, Bruce W. Weide
2011	J	`jnl`	Type inference in mathematics CoRR Jeremy Avigad
2011	J	`jnl`	Zen and the art of formalisation. Math. Struct. Comput. Sci. Andrea Asperti, Jeremy Avigad
2009	J	`jnl`	A Formal System for Euclid's Elements. Rev. Symb. Log. Jeremy Avigad, Edward T. Dean, John Mumma
2009	J	`jnl`	Functional interpretation and inductive definitions. J. Symb. Log. Jeremy Avigad, Henry Towsner
2009	J	`jnl`	The metamathematics of ergodic theory. Ann. Pure Appl. Log. Jeremy Avigad
2008	J	`jnl`	A language for mathematical language management CoRR Steven Kieffer, Jeremy Avigad, Harvey Friedman
2007	J	`jnl`	A Decision Procedure for Linear "Big O" Equations. J. Autom. Reason. Jeremy Avigad, Kevin Donnelly
2007	J	`jnl`	A decision procedure for linear "big O" equations CoRR Jeremy Avigad, Kevin Donnelly
2007	J	`jnl`	A formally verified proof of the prime number theorem. ACM Trans. Comput. Log. Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
2007	J	`jnl`	Quantifier elimination for the reals with a predicate for the powers of two. Theor. Comput. Sci. Jeremy Avigad, Yimu Yin
2006	J	`jnl`	Combining decision procedures for the reals CoRR Jeremy Avigad, Harvey Friedman
2006	J	`jnl`	Combining decision procedures for the reals. Log. Methods Comput. Sci. Jeremy Avigad, Harvey Friedman
2006	J	`jnl`	Fundamental notions of analysis in subsystems of second-order arithmetic. Ann. Pure Appl. Log. Jeremy Avigad, Ksenija Simic
2006	J	`jnl`	Mathematical Method and Proof. Synth. Jeremy Avigad
2006	J	`jnl`	Quantifier elimination for the reals with a predicate for the powers of two CoRR Jeremy Avigad, Yimu Yin
2005	J	`jnl`	A formally verified proof of the prime number theorem CoRR Jeremy Avigad, Kevin Donnelly, David Gray, Paul Raff
2005	J	`jnl`	Preface. Ann. Pure Appl. Log. Arnold Beckmann, Jeremy Avigad, Georg Moser
2004	J	`jnl`	Forcing in proof theory. Bull. Symb. Log. Jeremy Avigad
2004	A	`conf`	Formalizing O Notation in Isabelle/HOL. IJCAR Jeremy Avigad, Kevin Donnelly
2003	J	`jnl`	Eliminating definitions and Skolem functions in first-order logic. ACM Trans. Comput. Log. Jeremy Avigad
2003	J	`jnl`	Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234]. Ann. Pure Appl. Log. Jeremy Avigad
2002	J	`jnl`	An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal Notations. J. Math. Log. Jeremy Avigad
2002	J	`jnl`	Saturated models of universal theories. Ann. Pure Appl. Log. Jeremy Avigad
2002	J	`jnl`	Transfer principles in nonstandard intuitionistic arithmetic. Arch. Math. Log. Jeremy Avigad, Jeremy Helzner
2002	J	`jnl`	Update Procedures and the 1-Consistency of Arithmetic. Math. Log. Q. Jeremy Avigad
2001	J	`jnl`	Algebraic proofs of cut elimination. J. Log. Algebraic Methods Program. Jeremy Avigad
2001	A*	`conf`	Eliminating Definitions and Skolem Functions in First-Order Logic. LICS Jeremy Avigad
2001	J	`jnl`	Review of "Basic proof theory: second edition" by A. S. Troelstra and H. Schwichtenberg. Cambridge University Press. SIGACT News Jeremy Avigad
2000	J	`jnl`	Interpreting Classical Theories in Constructive Ones. J. Symb. Log. Jeremy Avigad
1999	J	`jnl`	The Model-Theoretic Ordinal Analysis of Theories of Predicative Strength. J. Symb. Log. Jeremy Avigad, Richard Sommer
1998	J	`jnl`	An effective proof that open sets are Ramsey. Arch. Math. Log. Jeremy Avigad
1998	J	`jnl`	Predicative Functionals and an Interpretation of ID Ann. Pure Appl. Log. Jeremy Avigad
1997	J	`jnl`	A model-theoretic approach to ordinal analysis. Bull. Symb. Log. Jeremy Avigad, Richard Sommer
1996	J	`jnl`	Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic. Ann. Pure Appl. Log. Jeremy Avigad
1996	J	`jnl`	On the Relationship Between ATR J. Symb. Log. Jeremy Avigad
1996	—	`conf`	Plausibly hard combinatorial tautologies. Proof Complexity and Feasible Arithmetics Jeremy Avigad