×

zbMATH — the first resource for mathematics

Avigad, Jeremy

Compute Distance To:
Author ID: avigad.jeremy Recent zbMATH articles by "Avigad, Jeremy"
Published as: Avigad, J.; Avigad, Jeremy
Homepage: http://www.andrew.cmu.edu/user/avigad/
External Links: MGP · Wikidata · ORCID · ResearchGate · dblp
Member of Collective: the-univalent-foundations-program.
Documents Indexed: 64 Publications since 1996, including 1 Book

Publications by Year

Citations contained in zbMATH

52 Publications have been cited 398 times in 314 Documents Cited by Year
Gödel’s functional (“Dialectica”) interpretation. Zbl 0913.03053
Avigad, Jeremy; Feferman, Solomon
49
1998
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
40
2013
A formal system for Euclid’s Elements. Zbl 1188.03008
Avigad, Jeremy; Dean, Edward; Mumma, John
33
2009
Local stability of ergodic averages. Zbl 1187.37010
Avigad, Jeremy; Gerhardy, Philipp; Towsner, Henry
22
2010
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
17
2015
Formalizing forcing arguments in subsystems of second-order arithmetic. Zbl 0860.03040
Avigad, Jeremy
17
1996
Interpreting classical theories in constructive ones. Zbl 0981.03061
Avigad, Jeremy
14
2000
A formally verified proof of the prime number theorem. Zbl 1367.68244
Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul
12
2007
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Zbl 1259.03021
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
11
2012
Forcing in proof theory. Zbl 1064.03034
Avigad, Jeremy
11
2004
On the relationship between \(ATR_ 0\) and \(\widehat {ID}_{<\omega}\). Zbl 0858.03052
Avigad, Jeremy
11
1996
Saturated models of universal theories. Zbl 1015.03040
Avigad, Jeremy
9
2002
Update procedures and the 1-consistency of arithmetic. Zbl 0988.03087
Avigad, Jeremy
9
2002
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
8
2015
Methodology and metaphysics in the development of Dedekind’s theory of ideals. Zbl 1164.00001
Avigad, Jeremy
8
2006
Mathematical method and proof. Zbl 1116.03012
Avigad, Jeremy
8
2006
An effective proof that open sets are Ramsey. Zbl 0909.03040
Avigad, Jeremy
8
1998
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
7
2012
Formalizing \(O\) notation in Isabelle/HOL. Zbl 1126.68557
Avigad, Jeremy; Donnelly, Kevin
7
2004
Eliminating definitions and Skolem functions in first-order logic. Zbl 1365.03038
Avigad, Jeremy
7
2003
Ultraproducts and metastability. Zbl 1321.46015
Avigad, Jeremy; Iovino, José
6
2013
Fundamental notions of analysis in subsystems of second-order arithmetic. Zbl 1109.03069
Avigad, Jeremy; Simic, Ksenija
6
2006
Number theory and elementary arithmetic. Zbl 1050.03005
Avigad, Jeremy
6
2003
Transfer principles in nonstandard intuitionistic arithmetic. Zbl 1024.03068
Avigad, J.; Helzner, J.
6
2002
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
5
2017
A model-theoretic approach to ordinal analysis. Zbl 0874.03068
Avigad, Jeremy; Sommer, Richard
5
1997
Functional interpretation and inductive definitions. Zbl 1193.03082
Avigad, Jeremy; Towsner, Henry
4
2009
The metamathematics of ergodic theory. Zbl 1168.03047
Avigad, Jeremy
4
2009
Weak theories of nonstandard arithmetic and analysis. Zbl 1087.03038
Avigad, Jeremy
4
2005
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Zbl 1355.37009
Avigad, Jeremy; Rute, Jason
3
2015
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression. Zbl 1296.01010
Avigad, Jeremy; Morris, Rebecca
3
2014
Uniform distribution and algorithmic randomness. Zbl 1275.03133
Avigad, Jeremy
3
2013
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
3
2012
Algebraic proofs of cut elimination. Zbl 1015.68174
Avigad, Jeremy
3
2001
The model-theoretic ordinal analysis of theories of predicative strength. Zbl 0939.03066
Avigad, Jeremy; Sommer, Richard
3
1999
Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\). Zbl 0945.03084
Avigad, Jeremy
3
1998
Character and object. Zbl 1427.01005
Avigad, Jeremy; Morris, Rebecca
2
2016
A heuristic prover for real inequalities. Zbl 1416.68149
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
2
2014
Zen and the art of formalisation. Zbl 1276.03002
Asperti, Andrea; Avigad, Jeremy
2
2011
Metastability in the Furstenberg-Zimmer tower. Zbl 1230.37004
Avigad, Jeremy; Towsner, Henry
2
2010
Quantifier elimination for the reals with a predicate for the powers of two. Zbl 1113.03027
Avigad, Jeremy; Yin, Yimu
2
2007
Combining decision procedures for the reals. Zbl 1127.03006
Avigad, Jeremy; Friedman, Harvey
2
2006
Plausibly hard combinatorial tautologies. Zbl 0891.03024
Avigad, Jeremy
2
1998
The mechanization of mathematics. Zbl 1398.68478
Avigad, Jeremy
1
2018
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. Zbl 1391.68001
Avigad, Jeremy (ed.); Mahboubi, Assia (ed.)
1
2018
A metastable dominated convergence theorem. Zbl 1277.28003
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
1
2012
Uncomputably noisy ergodic limits. Zbl 1258.03084
Avigad, Jeremy
1
2012
The computational content of classical arithmetic. Zbl 1244.03153
Avigad, Jeremy
1
2010
A decision procedure for linear “big O” equations. Zbl 1122.03004
Avigad, Jeremy; Donnelly, Kevin
1
2007
Ordinal analysis without proofs. Zbl 1008.03038
Avigad, Jeremy
1
2002
An ordinal analysis of admissible set theory using recursion on ordinal notations. Zbl 1016.03060
Avigad, Jeremy
1
2002
A realizability interpretation for classical arithmetic. Zbl 0946.03071
Avigad, Jeremy
1
2000
The mechanization of mathematics. Zbl 1398.68478
Avigad, Jeremy
1
2018
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. Zbl 1391.68001
Avigad, Jeremy (ed.); Mahboubi, Assia (ed.)
1
2018
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
5
2017
Character and object. Zbl 1427.01005
Avigad, Jeremy; Morris, Rebecca
2
2016
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
17
2015
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
8
2015
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Zbl 1355.37009
Avigad, Jeremy; Rute, Jason
3
2015
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression. Zbl 1296.01010
Avigad, Jeremy; Morris, Rebecca
3
2014
A heuristic prover for real inequalities. Zbl 1416.68149
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
2
2014
A machine-checked proof of the odd order theorem. Zbl 1317.68211
Gonthier, Georges; Asperti, Andrea; Avigad, Jeremy; Bertot, Yves; Cohen, Cyril; Garillot, François; Le Roux, Stéphane; Mahboubi, Assia; O’Connor, Russell; Ould Biha, Sidi; Pasca, Ioana; Rideau, Laurence; Solovyev, Alexey; Tassi, Enrico; Théry, Laurent
40
2013
Ultraproducts and metastability. Zbl 1321.46015
Avigad, Jeremy; Iovino, José
6
2013
Uniform distribution and algorithmic randomness. Zbl 1275.03133
Avigad, Jeremy
3
2013
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Zbl 1259.03021
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
11
2012
\(\delta \)-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
7
2012
\(\delta\)-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
3
2012
A metastable dominated convergence theorem. Zbl 1277.28003
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
1
2012
Uncomputably noisy ergodic limits. Zbl 1258.03084
Avigad, Jeremy
1
2012
Zen and the art of formalisation. Zbl 1276.03002
Asperti, Andrea; Avigad, Jeremy
2
2011
Local stability of ergodic averages. Zbl 1187.37010
Avigad, Jeremy; Gerhardy, Philipp; Towsner, Henry
22
2010
Metastability in the Furstenberg-Zimmer tower. Zbl 1230.37004
Avigad, Jeremy; Towsner, Henry
2
2010
The computational content of classical arithmetic. Zbl 1244.03153
Avigad, Jeremy
1
2010
A formal system for Euclid’s Elements. Zbl 1188.03008
Avigad, Jeremy; Dean, Edward; Mumma, John
33
2009
Functional interpretation and inductive definitions. Zbl 1193.03082
Avigad, Jeremy; Towsner, Henry
4
2009
The metamathematics of ergodic theory. Zbl 1168.03047
Avigad, Jeremy
4
2009
A formally verified proof of the prime number theorem. Zbl 1367.68244
Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul
12
2007
Quantifier elimination for the reals with a predicate for the powers of two. Zbl 1113.03027
Avigad, Jeremy; Yin, Yimu
2
2007
A decision procedure for linear “big O” equations. Zbl 1122.03004
Avigad, Jeremy; Donnelly, Kevin
1
2007
Methodology and metaphysics in the development of Dedekind’s theory of ideals. Zbl 1164.00001
Avigad, Jeremy
8
2006
Mathematical method and proof. Zbl 1116.03012
Avigad, Jeremy
8
2006
Fundamental notions of analysis in subsystems of second-order arithmetic. Zbl 1109.03069
Avigad, Jeremy; Simic, Ksenija
6
2006
Combining decision procedures for the reals. Zbl 1127.03006
Avigad, Jeremy; Friedman, Harvey
2
2006
Weak theories of nonstandard arithmetic and analysis. Zbl 1087.03038
Avigad, Jeremy
4
2005
Forcing in proof theory. Zbl 1064.03034
Avigad, Jeremy
11
2004
Formalizing \(O\) notation in Isabelle/HOL. Zbl 1126.68557
Avigad, Jeremy; Donnelly, Kevin
7
2004
Eliminating definitions and Skolem functions in first-order logic. Zbl 1365.03038
Avigad, Jeremy
7
2003
Number theory and elementary arithmetic. Zbl 1050.03005
Avigad, Jeremy
6
2003
Saturated models of universal theories. Zbl 1015.03040
Avigad, Jeremy
9
2002
Update procedures and the 1-consistency of arithmetic. Zbl 0988.03087
Avigad, Jeremy
9
2002
Transfer principles in nonstandard intuitionistic arithmetic. Zbl 1024.03068
Avigad, J.; Helzner, J.
6
2002
Ordinal analysis without proofs. Zbl 1008.03038
Avigad, Jeremy
1
2002
An ordinal analysis of admissible set theory using recursion on ordinal notations. Zbl 1016.03060
Avigad, Jeremy
1
2002
Algebraic proofs of cut elimination. Zbl 1015.68174
Avigad, Jeremy
3
2001
Interpreting classical theories in constructive ones. Zbl 0981.03061
Avigad, Jeremy
14
2000
A realizability interpretation for classical arithmetic. Zbl 0946.03071
Avigad, Jeremy
1
2000
The model-theoretic ordinal analysis of theories of predicative strength. Zbl 0939.03066
Avigad, Jeremy; Sommer, Richard
3
1999
Gödel’s functional (“Dialectica”) interpretation. Zbl 0913.03053
Avigad, Jeremy; Feferman, Solomon
49
1998
An effective proof that open sets are Ramsey. Zbl 0909.03040
Avigad, Jeremy
8
1998
Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\). Zbl 0945.03084
Avigad, Jeremy
3
1998
Plausibly hard combinatorial tautologies. Zbl 0891.03024
Avigad, Jeremy
2
1998
A model-theoretic approach to ordinal analysis. Zbl 0874.03068
Avigad, Jeremy; Sommer, Richard
5
1997
Formalizing forcing arguments in subsystems of second-order arithmetic. Zbl 0860.03040
Avigad, Jeremy
17
1996
On the relationship between \(ATR_ 0\) and \(\widehat {ID}_{<\omega}\). Zbl 0858.03052
Avigad, Jeremy
11
1996
all top 5

Cited by 420 Authors

19 Avigad, Jeremy
16 Kohlenbach, Ulrich Wilhelm
8 Oliva, Paulo
8 Sanders, Sam
7 Ferreira, Fernando
7 Towsner, Henry
6 Asperti, Andrea
6 Kapulkin, Krzysztof
6 Paulson, Lawrence Charles
5 Kaliszyk, Cezary
5 Kreuzer, Alexander P.
5 Safarik, Pavol
5 Sato, Kentaro
5 Van den Berg, Benno
4 Aschieri, Federico
4 Beeson, Michael J.
4 Gaspar, Jaime
4 Hernest, Mircea-Dan
4 Janičić, Predrag
4 Leuştean, Laurenţiu
4 Mumma, John
4 Narboux, Julien
4 Nipkow, Tobias
4 Rute, Jason
3 Arai, Toshiyasu
3 Ferreira, Gilda
3 Fujiwara, Makoto
3 Hetzl, Stefan
3 Kahle, Reinhard
3 Lumsdaine, Peter LeFanu
3 Morris, Rebecca Lea
3 Normann, Dag
3 Patey, Ludovic
3 Powell, Thomas M.
3 Rojas, Cristobal
3 Shafer, Paul
3 Szumiło, Karol
2 Affeldt, Reynald
2 Aransay, Jesús
2 Benedikt, Michael A.
2 Bickford, Mark
2 Bienvenu, Laurent
2 Blanchette, Jasmin Christian
2 Briseid, Eyvind Martol
2 Chan, Hing-Lun
2 Cockx, Jesper
2 Cohen, Cyril
2 Coquand, Thierry
2 Cordón-Franco, Andrés
2 Enayat, Ali
2 Feferman, Solomon
2 Ferreira, Fernando Fagundes
2 Franklin, Johanna N. Y.
2 Grosu, Radu
2 Hamami, Yacin
2 Heras, Jónathan
2 Hoyrup, Mathieu
2 Ilik, Danko
2 Islam, Md. Ariful
2 Kawai, Tatsuji
2 Kentaro, Sato
2 Kotlarski, Henryk
2 Kristiansen, Lars
2 Lara-Martín, Francisco Felix
2 Li, Wenda
2 Moniri, Morteza
2 Moser, Georg
2 Müller, Moritz
2 Negri, Sara
2 Nicolae, Adriana
2 Norrish, Michael
2 Pąk, Karol
2 Panza, Marco
2 Passmore, Grant Olney
2 Ricciotti, Wilmer
2 Sacerdoti Coen, Claudio
2 Siddique, Umair
2 Simpson, Stephen G.
2 Smolka, Scott A.
2 Stojanović Đurđević, Sana
2 Stojanović, Sana
2 Tahar, Sofiène
2 Weiermann, Andreas
2 Wenzel, Makarius
2 Wiedijk, Freek
2 Wong, Tin Lok
2 Yokoyama, Keita
1 Abel, Andreas M.
1 Aberdein, Andrew
1 Achourioti, Theodora
1 Adams, Mark
1 Adams, Mark F.
1 Adams, Robin
1 Afshari, Bahareh
1 Ahrens, Benedikt
1 Aisenberg, James
1 Alama, Jesse
1 Anand, Abhishek
1 Anatriello, Giuseppina
1 Angiuli, Carlo
...and 320 more Authors
all top 5

Cited in 72 Serials

45 Annals of Pure and Applied Logic
21 Journal of Automated Reasoning
20 The Journal of Symbolic Logic
20 Archive for Mathematical Logic
11 MSCS. Mathematical Structures in Computer Science
10 Synthese
9 The Bulletin of Symbolic Logic
8 Mathematical Logic Quarterly (MLQ)
6 Advances in Mathematics
6 Annals of Mathematics and Artificial Intelligence
6 The Review of Symbolic Logic
5 Notre Dame Journal of Formal Logic
5 Studia Logica
5 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
4 Proceedings of the American Mathematical Society
4 Theoretical Computer Science
4 Ergodic Theory and Dynamical Systems
4 Information and Computation
4 Indagationes Mathematicae. New Series
4 Theory of Computing Systems
3 Artificial Intelligence
3 Transactions of the American Mathematical Society
3 Journal of Functional Programming
3 Journal of Mathematical Logic
2 Archive for History of Exact Sciences
2 Journal of Mathematical Analysis and Applications
2 Journal of Pure and Applied Algebra
2 Journal of Symbolic Computation
2 Formal Aspects of Computing
2 Historia Mathematica
2 Communications in Contemporary Mathematics
2 The Journal of Logic and Algebraic Programming
2 ACM Transactions on Computational Logic
2 Journal of Applied Logic
2 Fixed Point Theory and Applications
2 Mathematics in Computer Science
2 Journal of Logic and Analysis
2 Journal of Formalized Reasoning
1 Israel Journal of Mathematics
1 Journal d’Analyse Mathématique
1 Mathematische Semesterberichte
1 Chaos, Solitons and Fractals
1 The Mathematical Intelligencer
1 Fuzzy Sets and Systems
1 Journal of Mathematical Economics
1 Topology and its Applications
1 Bulletin of the American Mathematical Society. New Series
1 Applicable Algebra in Engineering, Communication and Computing
1 Computational Optimization and Applications
1 Formal Methods in System Design
1 Journal of Logic, Language and Information
1 Applied Categorical Structures
1 Selecta Mathematica. New Series
1 Topoi
1 Journal for Geometry and Graphics
1 Chaos
1 Philosophical Transactions of the Royal Society of London. Series A. Mathematical, Physical and Engineering Sciences
1 Annals of Mathematics. Second Series
1 Foundations of Science
1 Foundations of Computational Mathematics
1 Theory and Practice of Logic Programming
1 JP Journal of Algebra, Number Theory and Applications
1 Proceedings of the Steklov Institute of Mathematics
1 Journal of Homotopy and Related Structures
1 Nonlinear Analysis. Hybrid Systems
1 Philosophy Compass
1 Forum of Mathematics, Pi
1 Transactions of the London Mathematical Society
1 Journal of Logical and Algebraic Methods in Programming
1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences
1 Higher Structures
1 British Journal for the History of Mathematics
all top 5

Cited in 38 Fields

225 Mathematical logic and foundations (03-XX)
100 Computer science (68-XX)
26 General and overarching topics; collections (00-XX)
20 History and biography (01-XX)
14 Operator theory (47-XX)
14 Geometry (51-XX)
13 Category theory; homological algebra (18-XX)
12 Dynamical systems and ergodic theory (37-XX)
10 Number theory (11-XX)
10 Real functions (26-XX)
10 Algebraic topology (55-XX)
9 Combinatorics (05-XX)
6 Group theory and generalizations (20-XX)
5 Measure and integration (28-XX)
5 Functional analysis (46-XX)
5 General topology (54-XX)
3 Systems theory; control (93-XX)
2 Order, lattices, ordered algebraic structures (06-XX)
2 Commutative algebra (13-XX)
2 Algebraic geometry (14-XX)
2 Probability theory and stochastic processes (60-XX)
2 Operations research, mathematical programming (90-XX)
2 Biology and other natural sciences (92-XX)
2 Mathematics education (97-XX)
1 Field theory and polynomials (12-XX)
1 Linear and multilinear algebra; matrix theory (15-XX)
1 Nonassociative rings and algebras (17-XX)
1 Functions of a complex variable (30-XX)
1 Ordinary differential equations (34-XX)
1 Partial differential equations (35-XX)
1 Approximations and expansions (41-XX)
1 Abstract harmonic analysis (43-XX)
1 Convex and discrete geometry (52-XX)
1 Differential geometry (53-XX)
1 Numerical analysis (65-XX)
1 Optics, electromagnetic theory (78-XX)
1 Game theory, economics, finance, and other social and behavioral sciences (91-XX)
1 Information and communication theory, circuits (94-XX)

Citations by Year

Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.