Jeremy Avigad | Academic Influence

Jeremy Avigad's AcademicInfluence.com Rankings

Jeremy Avigad

Mathematics

#4615

World Rank

#6534

Historical Rank

#1570

USA Rank

Measure Theory

#3205

World Rank

#3793

Historical Rank

#927

USA Rank

mathematics Degrees

Download Badge

Mathematics

Jeremy Avigad's Degrees

PhD Mathematics University of California, Berkeley
Bachelors Mathematics University of Chicago

Similar Degrees You Can Earn

Best Online Bachelor's in Math 2025

Why Is Jeremy Avigad Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Jeremy Avigad is a professor of philosophy and a professor of mathematical sciences at Carnegie Mellon University. He received a B.A. in mathematics from Harvard University in 1989, and a Ph.D. in mathematics from the University of California at Berkeley in 1995 under the supervision of Jack Silver. He has contributed to the areas of mathematical logic and foundations, formal verification and interactive theorem proving, and the philosophy and history of mathematics. He became Director of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University after Charles Hoskinson donated $20 Million in September 2021 to establish it.

(See a Problem?)

Jeremy Avigad's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

A Machine-Checked Proof of the Odd Order Theorem (2013) (338)
The Lean Theorem Prover (System Description) (2015) (322)
Proof Theory (2017) (264)
Chapter V – Gödel’s Functional (“Dialectica”) Interpretation (1998) (183)
δ-Complete Decision Procedures for Satisfiability over the Reals (2012) (173)
A FORMAL SYSTEM FOR EUCLID’S ELEMENTS (2008) (147)
LOCAL STABILITY OF ERGODIC AVERAGES (2007) (95)
A formally verified proof of the prime number theorem (2005) (93)
Computability and analysis: the legacy of Alan Turing (2012) (78)
Formally verified mathematics (2014) (76)
Delta-Decidability over the Reals (2012) (75)
Building a push-button RESOLVE verifier: Progress and challenges (2011) (73)
A metaprogramming framework for formal verification (2017) (72)
Mathematical Method and Proof (2006) (60)
Number theory and elementary arithmetic (2003) (56)
The Lean Theorem Prover (2015) (54)
Interpreting classical theories in constructive ones (2000) (48)
The hair follicle mites (Demodex spp.). Could they be vectors of pathogenic microorganisms? (1988) (45)
Formalizing Forcing Arguments in Subsystems of Second-Order Arithmetic (1996) (44)
Eliminating definitions and Skolem functions in first-order logic (2001) (37)
Algorithmic randomness, reverse mathematics, and the dominated convergence theorem (2011) (36)
A Formally Verified Proof of the Central Limit Theorem (2014) (35)
Formalizing O Notation in Isabelle/HOL (2004) (34)
Methodology and metaphysics in the development of Dedekind's theory of ideals (2005) (34)
Weak Theories of Nonstandard Arithmetic and Analysis (2000) (32)
Forcing in Proof Theory (2004) (31)
Review: Sergei N. Artemov, Explicit Provability and Constructive Semantics (2002) (30)
Homotopy limits in type theory (2013) (30)
Saturated models of universal theories (2002) (30)
Computers in Mathematical Inquiry (2008) (27)
Oscillation and the mean ergodic theorem for uniformly convex Banach spaces (2012) (27)
Update Procedures and the 1-Consistency of Arithmetic (2002) (27)
The birth of model theory: Lowenheim’s theorem in the frame of the theory of relatives (2006) (26)
On the Relationship Between ATR0 and ID (1996) (26)
Ultraproducts and metastability (2013) (24)
A Model-Theoretic Approach to Ordinal Analysis (1997) (24)
On the Relationships between $ATR_0$ And $\widehat{ID}_{< \omega}$ (1996) (24)
Theorem Proving in Lean (2016) (23)
On the Relationship Between ATR 0 and ID . (1996) (23)
Scabies: the diagnosis of atypical cases. (1995) (22)
The metamathematics of ergodic theory (2009) (22)
Fundamental notions of analysis in subsystems of second-order arithmetic (2006) (22)
A Variant of the Double-Negation Translation (2006) (19)
Reliability of mathematical inference (2020) (18)
Transfer principles in nonstandard intuitionistic arithmetic (2002) (17)
Algebraic proofs of cut elimination (2001) (17)
"Clarifying the Nature of the Infinite": the Development of Metamathematics and Proof Theory (2001) (17)
Combining decision procedures for the reals (2006) (16)
Functional interpretation and inductive definitions (2008) (16)
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression (2012) (15)
MODULARITY IN MATHEMATICS (2020) (15)
An effective proof that open sets are Ramsey (1998) (15)
A Realizability Interpretation for Classical Arithmetic (2002) (15)
Elaboration in Dependent Type Theory (2015) (14)
Uniform distribution and algorithmic randomness (2012) (11)
The model-theoretic ordinal analysis of theories of predicative strength (1999) (11)
Godel's functional interpretation (1998) (11)
A metastable dominated convergence theorem (2012) (11)
CHARACTER AND OBJECT (2014) (10)
A Language for Mathematical Knowledge Management (2008) (9)
A Heuristic Prover for Real Inequalities (2014) (9)
Quantifier elimination for the reals with a predicate for the powers of two (2006) (9)
Verifiably Safe Autonomy for Cyber-Physical Systems (2018) (8)
Understanding, formal verification, and the philosophy of mathematics (2010) (8)
Predicative Functionals and an Interpretation of ID (1998) (8)
Metastability in the Furstenberg-Zimmer Tower (2009) (8)
An Ordinal Analysis of Admissible Set Theory using Recursion on Ordinal Notations (2002) (7)
Notes on a Formalization of the Prime Number Theorem (2004) (7)
Homotopy limits in Coq (2013) (7)
The computational content of classical arithmetic (2009) (6)
Zen and the art of formalisation (2011) (6)
Opinion: The Mechanization of Mathematics (2018) (6)
Type inference in mathematics (2011) (5)
Immunotherapy of superficial dermatomycoses. (1973) (5)
Aspects of Ergodic Theory in Subsystems of (2004) (5)
Review of "Basic proof theory: second edition" by A. S. Troelstra and H. Schwichtenberg. Cambridge University Press. (2001) (5)
Plausibly hard combinatorial tautologies (1996) (5)
Data Types as Quotients of Polynomial Functors (2019) (5)
Uncomputably Noisy Ergodic Limits (2011) (5)
Dedekind's 1871 version of the theory of ideals ⁄ (2004) (4)
A Decision Procedure for Linear “Big O” Equations (2007) (4)
Some results of number theory (2009) (4)
Marcus Giaquinto. Visual Thinking in Mathematics: An Epistemological Study (2008) (4)
Introduction to Milestones in Interactive Theorem Proving (2018) (4)
Notes on II-conservativity, w-submodels, and the Collection Schema (2002) (4)
ORDINAL ANALYSIS WITHOUT PROOFS (2000) (4)
Philosophy of Mathematics (2007) (4)
Varieties of mathematical understanding (2021) (4)
A language for mathematical language management (2008) (4)
Oscillation and the mean ergodic theorem (2012) (3)
Classical and constructive logic (2001) (3)
On the relationship between ATR0 and (1996) (3)
Learning Logic and Proof with an Interactive Theorem Prover (2019) (3)
On the computability of graphons (2018) (3)
δ -Decidability over the Reals ∗ (2012) (3)
ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (2023) (3)
The Mechanization of Mathematics (2019) (3)
Inverting the Furstenberg correspondence (2011) (2)
Adding Soft Types to Isabelle (2018) (2)
Algorithmic barriers to representing conditional independence (2019) (2)
Interactive Theorem Proving (2018) (2)
ON COMPUTABLE REPRESENTATIONS OF EXCHANGEABLE DATA (2016) (2)
Zen and the art of formalization (2010) (2)
Gödel and the Metamathematical Tradition (2007) (2)
A Heuristic Prover for Real Inequalities (2016) (1)
On the Relationship Between ID^_ (1996) (1)
Automated Reasoning for the Working Mathematician (2019) (1)
[Immunotherapy of superficial dermatomycoses]. (1972) (1)
William Tait. The provenance of pure reason: essays in the philosophy of mathematics and its history . Oxford University Press, Oxford, 2005, x + 332 pp. (2006) (1)
Notes on Pi^1_1 Conservativity, Omega-Submodels, and the Collection Schema (2001) (1)
Mathematical Logic and Computation (2022) (1)
Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (2016) (1)
Erratum to "Saturated models of universal theories": [Ann. Pure Appl. Logic 118 (2002) 219-234] (2003) (1)
A verified algebraic representation of cairo program execution (2021) (1)
METASTABLE CONVERGENCE THEOREMS (2011) (1)
Progress On A Perimeter Surveillance Problem (2020) (1)
A Formally Verified Proof of the Central Limit Theorem (2017) (1)
2 3 A ug 2 00 7 Local stability of ergodic averages ∗ (0)
WINTER OF THE ASSOCIATION FOR SYMBOLIC LOGIC (2022) (0)
Verified reductions for optimization (2023) (0)
The Hilton New York Hotel New York, NY December 27–29, 2005 (2006) (0)
Ju n 20 07 Local stability of ergodic averages ∗ (0)
Reliability of mathematical inference (2020) (0)
Gnomes in the fog: The reception of brouwer’s intuitionism in the 1920s (2006) (0)
An Impossible Asylum (2021) (0)
Type Theory, Computation and Interactive Theorem Proving (2015) (0)
Smullyan Raymond M.. First-order logic. Corrected republication of XL 237. Dover Publications, New York 1995, xii + 158 pp. (1996) (0)
Hjorth, G., Kechris, AS and Louveau, A., Bore1 equivalence (1998) (0)
Logic's Lost Genius and Gentzen's Centenary (2016) (0)
2 M ay 2 00 8 Local stability of ergodic averages ∗ (0)
16w5072: Algorithmic Randomness Interacts with Analysis and Ergodic Theory (2017) (0)
L O ] 8 J ul 2 01 5 HOMOTOPY LIMITS IN TYPE THEORY (2015) (0)
Verified Optimization (2021) (0)
Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp (2014) (0)
Mathematics and Language (2015) (0)
A Thesis Proposal on Final Coalgebras (1998) (0)
Arai Toshiyasu. Some results on cut-elimination, provable well-orderings, induction and reflection. Annals of pure and applied logic , vol. 95 (1998), pp. 93–184. (2001) (0)
2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium '02 (2003) (0)
TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE (2022) (0)
S PECIAL I SSUE : I NTERACTIVE T HEOREM P ROVING AND THE F ORMALISATION OF M ATHEMATICS G UEST E DITORS : A NDREA A SPERTI AND J EREMY A VIGAD (2011) (0)
Bondy's Theorem (2012) (0)
Book review (1997) (0)
Theorem Proving with the Inverse Method for Linear Logic (2004) (0)
A formally verifled proof of the prime number theorem (2005) (0)
Artemov Sergei N.. Explicit provability and constructive semantics. The bulletin of symbolic logic , vol. 7 (2001), pp. 1–36. (2002) (0)
In the Light of Logic (1999) (0)
The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression (2013) (0)
Handbook of Practical Logic and Automated Reasoning, John Harrison, Cambridge University Press, 2009. Hardcover, ISBN-13: 978-0-521-89957-4, 681 pp. + xix, $135.00 (2010) (0)
The Computational Content of Classical Arithmetic to Appear in a Festschrift for Grigori Mints (2009) (0)
The Book Review Column 4. Analysis of Algorithms:an Active Learning Approach 5 Further Reading 6 Opinion (2002) (0)
Philosophy of Mathematics: 5 Questions (2007) (0)
Review: Raymond M. Smullyan, First-Order Logic (1996) (0)
The mathematical context behind Frege ’ s analysis of function and object ∗ (2014) (0)
FOUNDATIONS (1971) (0)
A pr 2 01 2 δ-Decidability over the Reals ∗ (2012) (0)
Scholarly Publishers: Scholars or Crooks? (2012) (0)
Notices (1978) (0)
Erratum to: Interactive Theorem Proving (2018) (0)
Plato’s Ghost: The Modernist Transformation of Mathematics by Jeremy Gray (2010) (0)
Notes on Chapters 3 and 4 of Dedekind’s Theory of Algebraic Integers (2002) (0)
The design of mathematical language (2021) (0)
of Arai ’ s Some results on cut-elimination , provable well-orderings , induction , and reflection ∗ (2000) (0)
New Orleans Marriott and Sheraton New Orleans Hotels New Orleans, LA January 8–9, 2011 (2012) (0)
Preface: Selected Extended Papers from Interactive Theorem Proving 2018 (2020) (0)
on Chapter 2 of Dedekind ’ s Theory of Algebraic Integers (2002) (0)
Pilot study into the methods of assessing the effectiveness of social work intervention (SWI) in the management of the stroke family (1985) (0)
The Westin Seattle, Seattle, Washington March 28–29, 2002 (2002) (0)
THE HISTORY OF DIRICHLET ’ S THEOREM ON PRIMES IN AN ARITHMETIC PROGRESSION (2016) (0)
’ s Lost Genius and Gentzen ’ s Centenary A Dual Review by Jeremy Avigad (2016) (0)
Introduction to Milestones in Interactive Theorem Proving (2018) (0)
Palmer House Hilton Hotel, Chicago, Illinois April 23–24, 2004 (2004) (0)
Alan Turing: His Work and Impact, A Book Review (2014) (0)

This paper list is powered by the following services:

Other Resources About Jeremy Avigad

en.wikipedia.org

What Schools Are Affiliated With Jeremy Avigad?

Jeremy Avigad is affiliated with the following schools:

Image Attributions

Image Source for Jeremy Avigad