Jeremy Avigad

MaRDI QIDQ287376zbMATH OpenDBLPORCIDWikidataFDO

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Duper: a proof-producing superposition theorem prover for dependent type theory	2026-02-10	Paper
Anatomy of a formal proof Notices of the American Mathematical Society	2025-12-05	Paper
Algorithmic barriers to representing conditional independence	2024-12-19	Paper
A proof-producing compiler for blockchain applications	2024-11-26	Paper
Certified knowledge compilation with application to verified model counting	2024-11-26	Paper
What we talk about when we talk about mathematics	2024-10-24	Paper
Mathematics and language	2024-09-06	Paper
Verified reductions for optimization	2024-04-05	Paper
Mathematics and the formal turn Bulletin of the American Mathematical Society	2024-04-03	Paper
TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE The Review of Symbolic Logic	2024-01-11	Paper
An Impossible Asylum The American Mathematical Monthly	2023-05-11	Paper
Reliability of mathematical inference Synthese	2023-03-31	Paper
Mathematical Logic and Computation	2022-08-01	Paper
Varieties of mathematical understanding Bulletin of the American Mathematical Society	2021-11-19	Paper
Foundations	2020-09-20	Paper
Modularity in mathematics The Review of Symbolic Logic	2020-03-25	Paper
Opinion: The Mechanization of Mathematics Notices of the American Mathematical Society	2018-11-02	Paper
A formally verified proof of the central limit theorem Journal of Automated Reasoning	2018-02-02	Paper
On the computability of graphons	2018-01-31	Paper
Proof Theory	2017-11-06	Paper
Eliminating definitions and Skolem functions in first-order logic ACM Transactions on Computational Logic	2017-06-13	Paper
Character and object The Review of Symbolic Logic	2017-05-31	Paper
\(\delta\)-decidability over the reals 2012 27th Annual IEEE Symposium on Logic in Computer Science	2017-05-16	Paper
Logic's Lost Genius and Gentzen's Centenary Notices of the American Mathematical Society	2017-01-02	Paper
Homotopy limits in type theory Mathematical Structures in Computer Science	2016-07-27	Paper
Book review of: S. B. Cooper (ed.) and J. van Leeuwen (ed.), Alan Turing. His work and impact Notices of the American Mathematical Society	2016-06-15	Paper
A heuristic prover for real inequalities Journal of Automated Reasoning	2016-05-26	Paper
Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs The Bulletin of Symbolic Logic	2016-03-18	Paper
The Lean theorem prover (system description) Automated Deduction - CADE-25	2015-12-02	Paper
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces Ergodic Theory and Dynamical Systems	2015-07-13	Paper
A heuristic prover for real inequalities Interactive Theorem Proving	2014-09-08	Paper
The concept of ``character in Dirichlet's theorem on primes in an arithmetic progression Archive for History of Exact Sciences	2014-07-01	Paper
Ultraproducts and metastability The New York Journal of Mathematics	2014-03-14	Paper
Ultraproducts and metastability The New York Journal of Mathematics	2014-03-14	Paper
Understanding, formal verification, and the philosophy of mathematics (available as arXiv preprint)	2013-10-04	Paper
A machine-checked proof of the odd order theorem Interactive Theorem Proving	2013-08-07	Paper
Uniform distribution and algorithmic randomness Journal of Symbolic Logic	2013-04-23	Paper
Uniform distribution and algorithmic randomness Journal of Symbolic Logic	2013-04-23	Paper
Uniform distribution and algorithmic randomness Journal of Symbolic Logic	2013-04-23	Paper
Type inference in mathematics (available as arXiv preprint)	2013-01-28	Paper
A metastable dominated convergence theorem Journal of Logic and Analysis	2012-12-17	Paper
Uncomputably noisy ergodic limits Notre Dame Journal of Formal Logic	2012-11-23	Paper
Uncomputably noisy ergodic limits Notre Dame Journal of Formal Logic	2012-11-23	Paper
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem Annals of Pure and Applied Logic	2012-10-11	Paper
\(\delta \)-complete decision procedures for satisfiability over the reals Automated Reasoning	2012-09-05	Paper
\(\delta \)-complete decision procedures for satisfiability over the reals Automated Reasoning	2012-09-05	Paper
Inverting the Furstenberg correspondence Discrete and Continuous Dynamical Systems	2012-08-24	Paper
Computability and analysis: the legacy of Alan Turing	2012-06-15	Paper
Zen and the art of formalisation Mathematical Structures in Computer Science	2011-10-21	Paper
The computational content of classical arithmetic (available as arXiv preprint)	2011-05-31	Paper
scientific article; zbMATH DE number 5859773 (Why is no real title available?)	2011-03-02	Paper
Metastability in the Furstenberg-Zimmer tower Fundamenta Mathematicae	2011-01-11	Paper
Local stability of ergodic averages Transactions of the American Mathematical Society	2010-02-02	Paper
A FORMAL SYSTEM FOR EUCLID’SELEMENTS The Review of Symbolic Logic	2010-01-21	Paper
Functional interpretation and inductive definitions Journal of Symbolic Logic	2010-01-07	Paper
The metamathematics of ergodic theory Annals of Pure and Applied Logic	2009-03-25	Paper
scientific article; zbMATH DE number 5204708 (Why is no real title available?)	2007-10-24	Paper
Combining decision procedures for the reals Logical Methods in Computer Science	2007-10-11	Paper
Automated Reasoning Lecture Notes in Computer Science	2007-09-25	Paper
A decision procedure for linear ``big O equations Journal of Automated Reasoning	2007-08-17	Paper
Quantifier elimination for the reals with a predicate for the powers of two Theoretical Computer Science	2007-02-26	Paper
Mathematical method and proof Synthese	2006-12-20	Paper
Fundamental notions of analysis in subsystems of second-order arithmetic Annals of Pure and Applied Logic	2006-04-28	Paper
scientific article; zbMATH DE number 2236625 (Why is no real title available?)	2005-12-08	Paper
Forcing in Proof Theory The Bulletin of Symbolic Logic	2005-05-24	Paper
Number theory and elementary arithmetic† Philosophia Mathematica	2004-06-10	Paper
Transfer principles in nonstandard intuitionistic arithmetic Archive for Mathematical Logic	2003-09-16	Paper
AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS Journal of Mathematical Logic	2003-07-25	Paper
Saturated models of universal theories Annals of Pure and Applied Logic	2003-03-09	Paper
scientific article; zbMATH DE number 1870411 (Why is no real title available?)	2003-02-18	Paper
Update procedures and the 1-consistency of arithmetic Mathematical Logic Quarterly (MLQ)	2002-07-22	Paper
Algebraic proofs of cut elimination The Journal of Logic and Algebraic Programming	2002-05-21	Paper
Interpreting classical theories in constructive ones The Journal of Symbolic Logic	2002-03-11	Paper
scientific article; zbMATH DE number 1420833 (Why is no real title available?)	2000-10-22	Paper
Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) Annals of Pure and Applied Logic	1999-08-16	Paper
The model-theoretic ordinal analysis of theories of predicative strength Journal of Symbolic Logic	1999-06-29	Paper
An effective proof that open sets are Ramsey Archive for Mathematical Logic	1999-03-25	Paper
scientific article; zbMATH DE number 1215497 (Why is no real title available?)	1998-12-08	Paper
scientific article; zbMATH DE number 1114014 (Why is no real title available?)	1998-07-08	Paper
A Model-Theoretic Approach to Ordinal Analysis The Bulletin of Symbolic Logic	1997-11-05	Paper
Formalizing forcing arguments in subsystems of second-order arithmetic Annals of Pure and Applied Logic	1997-01-26	Paper
On the relationship between ATR0 and Journal of Symbolic Logic	1996-12-12	Paper

Research outcomes over time

This page was built for person: Jeremy Avigad