# zbMATH — the first resource for mathematics

Compute Distance To:
 Documents Indexed: 64 Publications since 1996, including 1 Book
all top 5

#### Co-Authors

 32 single-authored 3 Dean, Edward T. 3 Donnelly, Kevin P. 3 Mahboubi, Assia 3 Rute, Jason 3 Towsner, Henry 2 Asperti, Andrea 2 Clarke, Edmund Melson jun. 2 Gao, Sicun 2 Lewis, Robert Y. 2 Morris, Rebecca Lea 2 Roux, Cody 2 Sommer, Richard 1 Bertot, Yves 1 Blanchette, Jasmin Christian 1 Cohen, Cyril 1 de Moura, Leonardo 1 Feferman, Solomon 1 Friedman, Harvey M. 1 Garillot, François 1 Gerhardy, Philipp 1 Gonthier, Georges 1 Gray, David F. 1 Helzner, Jeffrey 1 Hölzl, Johannes 1 Iovino, José N. 1 Kapulkin, Krzysztof 1 Klein, Gerwin 1 Kong, Soonho 1 Leroux, Stéphane 1 Lumsdaine, Peter LeFanu 1 Mumma, John 1 O’Connor, Russell 1 Ould Biha, Sidi 1 Paşca, Ioana 1 Paulson, Lawrence Charles 1 Popescu, Andrei 1 Raff, Paul 1 Rideau, Laurence 1 Serafin, Luke 1 Simic, Ksenija 1 Snelting, Gregor 1 Solovyev, Alexey 1 Tassi, Enrico 1 Théry, Laurent 1 van Doorn, Floris 1 von Raumer, Jakob 1 Yin, Yimu
all top 5

#### Serials

 6 Annals of Pure and Applied Logic 5 The Journal of Symbolic Logic 5 Journal of Automated Reasoning 4 The Bulletin of Symbolic Logic 3 Notices of the American Mathematical Society 3 The Review of Symbolic Logic 2 MSCS. Mathematical Structures in Computer Science 2 Archive for Mathematical Logic 2 ACM Transactions on Computational Logic 1 Archive for History of Exact Sciences 1 Fundamenta Mathematicae 1 Notre Dame Journal of Formal Logic 1 Synthese 1 Theoretical Computer Science 1 Transactions of the American Mathematical Society 1 Ergodic Theory and Dynamical Systems 1 Mathematical Logic Quarterly (MLQ) 1 The New York Journal of Mathematics 1 Discrete and Continuous Dynamical Systems 1 Philosophia Mathematica. Series III 1 Bulletin of the European Association for Theoretical Computer Science EATCS 1 Journal of Mathematical Logic 1 The Journal of Logic and Algebraic Programming 1 Lecture Notes in Computer Science 1 Logical Methods in Computer Science 1 Journal of Logic and Analysis
all top 5

#### Fields

 53 Mathematical logic and foundations (03-XX) 18 Computer science (68-XX) 14 General and overarching topics; collections (00-XX) 8 History and biography (01-XX) 7 Dynamical systems and ergodic theory (37-XX) 4 Number theory (11-XX) 3 Group theory and generalizations (20-XX) 2 Operator theory (47-XX) 1 Field theory and polynomials (12-XX) 1 Associative rings and algebras (16-XX) 1 Category theory; homological algebra (18-XX) 1 Real functions (26-XX) 1 Measure and integration (28-XX) 1 Functions of a complex variable (30-XX) 1 Functional analysis (46-XX) 1 Geometry (51-XX) 1 Convex and discrete geometry (52-XX) 1 Algebraic topology (55-XX) 1 Probability theory and stochastic processes (60-XX) 1 Information and communication theory, circuits (94-XX)

#### 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
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
2013
A formal system for Euclid’s Elements. Zbl 1188.03008
Avigad, Jeremy; Dean, Edward; Mumma, John
2009
Local stability of ergodic averages. Zbl 1187.37010
Avigad, Jeremy; Gerhardy, Philipp; Towsner, Henry
2010
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
2015
Formalizing forcing arguments in subsystems of second-order arithmetic. Zbl 0860.03040
1996
Interpreting classical theories in constructive ones. Zbl 0981.03061
2000
A formally verified proof of the prime number theorem. Zbl 1367.68244
Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul
2007
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Zbl 1259.03021
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
2012
Forcing in proof theory. Zbl 1064.03034
2004
On the relationship between $$ATR_ 0$$ and $$\widehat {ID}_{<\omega}$$. Zbl 0858.03052
1996
Saturated models of universal theories. Zbl 1015.03040
2002
Update procedures and the 1-consistency of arithmetic. Zbl 0988.03087
2002
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
2015
Methodology and metaphysics in the development of Dedekind’s theory of ideals. Zbl 1164.00001
2006
Mathematical method and proof. Zbl 1116.03012
2006
An effective proof that open sets are Ramsey. Zbl 0909.03040
1998
$$\delta$$-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
2012
Formalizing $$O$$ notation in Isabelle/HOL. Zbl 1126.68557
2004
Eliminating definitions and Skolem functions in first-order logic. Zbl 1365.03038
2003
Ultraproducts and metastability. Zbl 1321.46015
2013
Fundamental notions of analysis in subsystems of second-order arithmetic. Zbl 1109.03069
2006
Number theory and elementary arithmetic. Zbl 1050.03005
2003
Transfer principles in nonstandard intuitionistic arithmetic. Zbl 1024.03068
2002
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
2017
A model-theoretic approach to ordinal analysis. Zbl 0874.03068
1997
Functional interpretation and inductive definitions. Zbl 1193.03082
2009
The metamathematics of ergodic theory. Zbl 1168.03047
2009
Weak theories of nonstandard arithmetic and analysis. Zbl 1087.03038
2005
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Zbl 1355.37009
2015
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression. Zbl 1296.01010
2014
Uniform distribution and algorithmic randomness. Zbl 1275.03133
2013
$$\delta$$-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
2012
Algebraic proofs of cut elimination. Zbl 1015.68174
2001
The model-theoretic ordinal analysis of theories of predicative strength. Zbl 0939.03066
1999
Predicative functionals and an interpretation of $${\widehat{\text{ID}}_{<\omega}}$$. Zbl 0945.03084
1998
Character and object. Zbl 1427.01005
2016
A heuristic prover for real inequalities. Zbl 1416.68149
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
2014
Zen and the art of formalisation. Zbl 1276.03002
2011
Metastability in the Furstenberg-Zimmer tower. Zbl 1230.37004
2010
Quantifier elimination for the reals with a predicate for the powers of two. Zbl 1113.03027
2007
Combining decision procedures for the reals. Zbl 1127.03006
2006
Plausibly hard combinatorial tautologies. Zbl 0891.03024
1998
The mechanization of mathematics. Zbl 1398.68478
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.)
2018
A metastable dominated convergence theorem. Zbl 1277.28003
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
2012
Uncomputably noisy ergodic limits. Zbl 1258.03084
2012
The computational content of classical arithmetic. Zbl 1244.03153
2010
A decision procedure for linear “big O” equations. Zbl 1122.03004
2007
Ordinal analysis without proofs. Zbl 1008.03038
2002
An ordinal analysis of admissible set theory using recursion on ordinal notations. Zbl 1016.03060
2002
A realizability interpretation for classical arithmetic. Zbl 0946.03071
2000
The mechanization of mathematics. Zbl 1398.68478
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.)
2018
A formally verified proof of the central limit theorem. Zbl 1425.68369
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke
2017
Character and object. Zbl 1427.01005
2016
The Lean theorem prover (system description). Zbl 06515520
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
2015
Homotopy limits in type theory. Zbl 1362.18004
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu
2015
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. Zbl 1355.37009
2015
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression. Zbl 1296.01010
2014
A heuristic prover for real inequalities. Zbl 1416.68149
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody
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
2013
Ultraproducts and metastability. Zbl 1321.46015
2013
Uniform distribution and algorithmic randomness. Zbl 1275.03133
2013
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. Zbl 1259.03021
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
2012
$$\delta$$-complete decision procedures for satisfiability over the reals. Zbl 1358.03028
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
2012
$$\delta$$-decidability over the reals. Zbl 1364.03065
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M.
2012
A metastable dominated convergence theorem. Zbl 1277.28003
Avigad, Jeremy; Dean, Edward T.; Rute, Jason
2012
Uncomputably noisy ergodic limits. Zbl 1258.03084
2012
Zen and the art of formalisation. Zbl 1276.03002
2011
Local stability of ergodic averages. Zbl 1187.37010
Avigad, Jeremy; Gerhardy, Philipp; Towsner, Henry
2010
Metastability in the Furstenberg-Zimmer tower. Zbl 1230.37004
2010
The computational content of classical arithmetic. Zbl 1244.03153
2010
A formal system for Euclid’s Elements. Zbl 1188.03008
Avigad, Jeremy; Dean, Edward; Mumma, John
2009
Functional interpretation and inductive definitions. Zbl 1193.03082
2009
The metamathematics of ergodic theory. Zbl 1168.03047
2009
A formally verified proof of the prime number theorem. Zbl 1367.68244
Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul
2007
Quantifier elimination for the reals with a predicate for the powers of two. Zbl 1113.03027
2007
A decision procedure for linear “big O” equations. Zbl 1122.03004
2007
Methodology and metaphysics in the development of Dedekind’s theory of ideals. Zbl 1164.00001
2006
Mathematical method and proof. Zbl 1116.03012
2006
Fundamental notions of analysis in subsystems of second-order arithmetic. Zbl 1109.03069
2006
Combining decision procedures for the reals. Zbl 1127.03006
2006
Weak theories of nonstandard arithmetic and analysis. Zbl 1087.03038
2005
Forcing in proof theory. Zbl 1064.03034
2004
Formalizing $$O$$ notation in Isabelle/HOL. Zbl 1126.68557
2004
Eliminating definitions and Skolem functions in first-order logic. Zbl 1365.03038
2003
Number theory and elementary arithmetic. Zbl 1050.03005
2003
Saturated models of universal theories. Zbl 1015.03040
2002
Update procedures and the 1-consistency of arithmetic. Zbl 0988.03087
2002
Transfer principles in nonstandard intuitionistic arithmetic. Zbl 1024.03068
2002
Ordinal analysis without proofs. Zbl 1008.03038
2002
An ordinal analysis of admissible set theory using recursion on ordinal notations. Zbl 1016.03060
2002
Algebraic proofs of cut elimination. Zbl 1015.68174
2001
Interpreting classical theories in constructive ones. Zbl 0981.03061
2000
A realizability interpretation for classical arithmetic. Zbl 0946.03071
2000
The model-theoretic ordinal analysis of theories of predicative strength. Zbl 0939.03066
1999
Gödel’s functional (“Dialectica”) interpretation. Zbl 0913.03053
1998
An effective proof that open sets are Ramsey. Zbl 0909.03040
1998
Predicative functionals and an interpretation of $${\widehat{\text{ID}}_{<\omega}}$$. Zbl 0945.03084
1998
Plausibly hard combinatorial tautologies. Zbl 0891.03024
1998
A model-theoretic approach to ordinal analysis. Zbl 0874.03068
1997
Formalizing forcing arguments in subsystems of second-order arithmetic. Zbl 0860.03040
1996
On the relationship between $$ATR_ 0$$ and $$\widehat {ID}_{<\omega}$$. Zbl 0858.03052
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)

#### Wikidata Timeline

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