Avigad, Jeremy; Baek, Seulkee; Bentkamp, Alexander; Heule, Marijn; Nawrocki, Wojciech An impossible asylum. (English) Zbl 07684392 Am. Math. Mon. 130, No. 5, 446-453 (2023). MSC: 03-01 03B35 68V15 PDF BibTeX XML Cite \textit{J. Avigad} et al., Am. Math. Mon. 130, No. 5, 446--453 (2023; Zbl 07684392) Full Text: DOI arXiv
Avigad, Jeremy Mathematical logic and computation. (English) Zbl 07565705 Cambridge: Cambridge University Press (ISBN 978-1-108-47875-5/hbk; 978-1-108-77875-6/ebook). xii, 513 p. (2023). MSC: 03-01 03Dxx 03Fxx 68-01 68Vxx PDF BibTeX XML Cite \textit{J. Avigad}, Mathematical logic and computation. Cambridge: Cambridge University Press (2023; Zbl 07565705) Full Text: DOI
Avigad, Jeremy Varieties of mathematical understanding. (English) Zbl 1482.00005 Bull. Am. Math. Soc., New Ser. 59, No. 1, 99-117 (2022). Reviewer: Truong Hoang Le (Hanoi) MSC: 00A30 01A67 52-02 52-08 68Vxx PDF BibTeX XML Cite \textit{J. Avigad}, Bull. Am. Math. Soc., New Ser. 59, No. 1, 99--117 (2022; Zbl 1482.00005) Full Text: DOI
Avigad, Jeremy Reliability of mathematical inference. (English) Zbl 1507.00016 Synthese 198, No. 8, 7377-7399 (2021). MSC: 00A30 PDF BibTeX XML Cite \textit{J. Avigad}, Synthese 198, No. 8, 7377--7399 (2021; Zbl 1507.00016) Full Text: DOI
Avigad, Jeremy (ed.); Mahboubi, Assia (ed.) Preface: Selected extended papers from Interactive Theorem Proving 2018. (English) Zbl 1468.68004 J. Autom. Reasoning 64, No. 5, 793-794 (2020). MSC: 68-06 68V15 00B25 PDF BibTeX XML Cite \textit{J. Avigad} (ed.) and \textit{A. Mahboubi} (ed.), J. Autom. Reasoning 64, No. 5, 793--794 (2020; Zbl 1468.68004) Full Text: DOI
Avigad, Jeremy Modularity in mathematics. (English) Zbl 1439.00026 Rev. Symb. Log. 13, No. 1, 47-79 (2020). Reviewer: Franz Lemmermeyer (Jagstzell) MSC: 00A30 00A35 03A05 PDF BibTeX XML Cite \textit{J. Avigad}, Rev. Symb. Log. 13, No. 1, 47--79 (2020; Zbl 1439.00026) Full Text: DOI
Avigad, Jeremy; Carneiro, Mario; Hudon, Simon Data types as quotients of polynomial functors. (English) Zbl 07649955 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 6, 19 p. (2019). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Avigad} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 6, 19 p. (2019; Zbl 07649955) Full Text: DOI
Avigad, Jeremy The mechanization of mathematics. (English) Zbl 1398.68478 Notices Am. Math. Soc. 65, No. 6, 681-690 (2018). MSC: 68T15 01A05 01A80 68-03 PDF BibTeX XML Cite \textit{J. Avigad}, Notices Am. Math. Soc. 65, No. 6, 681--690 (2018; Zbl 1398.68478) Full Text: DOI
Avigad, Jeremy (ed.); Blanchette, Jasmin Christian (ed.); Klein, Gerwin (ed.); Paulson, Lawrence (ed.); Popescu, Andrei (ed.); Snelting, Gregor (ed.) Introduction to “Milestones in interactive theorem proving”. (English) Zbl 1398.00118 J. Autom. Reasoning 61, No. 1-4, 1-8 (2018). MSC: 00B30 68-06 68T15 PDF BibTeX XML Cite \textit{J. Avigad} (ed.) et al., J. Autom. Reasoning 61, No. 1--4, 1--8 (2018; Zbl 1398.00118) Full Text: DOI Link
Avigad, Jeremy (ed.); Mahboubi, Assia (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. (English) Zbl 1391.68001 Lecture Notes in Computer Science 10895. Cham: Springer (ISBN 978-3-319-94820-1/pbk; 978-3-319-94821-8/ebook). xvii, 642 p. (2018). MSC: 68-06 68T15 00B25 PDF BibTeX XML Cite \textit{J. Avigad} (ed.) and \textit{A. Mahboubi} (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. Cham: Springer (2018; Zbl 1391.68001) Full Text: DOI
Avigad, Jeremy; Hölzl, Johannes; Serafin, Luke A formally verified proof of the central limit theorem. (English) Zbl 1425.68369 J. Autom. Reasoning 59, No. 4, 389-423 (2017). MSC: 68T15 60F05 PDF BibTeX XML Cite \textit{J. Avigad} et al., J. Autom. Reasoning 59, No. 4, 389--423 (2017; Zbl 1425.68369) Full Text: DOI arXiv
Avigad, Jeremy; Morris, Rebecca Character and object. (English) Zbl 1427.01005 Rev. Symb. Log. 9, No. 3, 480-510 (2016). Reviewer: Robert W. van der Waall (Amsterdam) MSC: 01A55 03-03 00A30 03A05 03F07 11-03 11M06 11M32 11N13 20C15 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{R. Morris}, Rev. Symb. Log. 9, No. 3, 480--510 (2016; Zbl 1427.01005) Full Text: DOI arXiv
Avigad, Jeremy Book review of: E. Menzler-Trott, Logic’s lost genius. The life of Gerhard Gentzen; and: R. Kahle (ed.) and M. Rathjen (ed.), Gentzen’s centenary. The quest for consistency. (English) Zbl 1352.00009 Notices Am. Math. Soc. 63, No. 11, 1288-1292 (2016). MSC: 00A17 01A70 01A60 01-02 03-03 03-06 03Fxx 03A05 00B15 PDF BibTeX XML Cite \textit{J. Avigad}, Notices Am. Math. Soc. 63, No. 11, 1288--1292 (2016; Zbl 1352.00009) Full Text: DOI
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody A heuristic prover for real inequalities. (English) Zbl 1356.68174 J. Autom. Reasoning 56, No. 3, 367-386 (2016). MSC: 68T15 26D07 68T20 PDF BibTeX XML Cite \textit{J. Avigad} et al., J. Autom. Reasoning 56, No. 3, 367--386 (2016; Zbl 1356.68174) Full Text: DOI arXiv
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu Homotopy limits in type theory. (English) Zbl 1362.18004 Math. Struct. Comput. Sci. 25, No. 5, 1040-1070 (2015). MSC: 18A15 03B15 55U40 68T15 PDF BibTeX XML Cite \textit{J. Avigad} et al., Math. Struct. Comput. Sci. 25, No. 5, 1040--1070 (2015; Zbl 1362.18004) Full Text: DOI arXiv
Avigad, Jeremy (ed.) 2014 European summer meeting of the Association for Symbolic Logic. Logic colloquium ’14, Vienna, Austria, July 14–19, 2014. (English) Zbl 1331.03004 Bull. Symb. Log. 21, No. 1, 34-103 (2015). MSC: 03-06 00B05 PDF BibTeX XML Cite \textit{J. Avigad} (ed.), Bull. Symb. Log. 21, No. 1, 34--103 (2015; Zbl 1331.03004) Full Text: DOI
de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob The Lean theorem prover (system description). (English) Zbl 1465.68279 Felty, Amy P. (ed.) et al., Automated deduction – CADE-25. 25th international conference on automated deduction, Berlin, Germany, August 1–7, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9195, 378-388 (2015). MSC: 68V15 68V20 PDF BibTeX XML Cite \textit{L. de Moura} et al., Lect. Notes Comput. Sci. 9195, 378--388 (2015; Zbl 1465.68279) Full Text: DOI Link
Avigad, Jeremy; Rute, Jason Oscillation and the mean ergodic theorem for uniformly convex Banach spaces. (English) Zbl 1355.37009 Ergodic Theory Dyn. Syst. 35, No. 4, 1009-1027 (2015). MSC: 37A30 47A35 47L10 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{J. Rute}, Ergodic Theory Dyn. Syst. 35, No. 4, 1009--1027 (2015; Zbl 1355.37009) Full Text: DOI arXiv
Avigad, Jeremy Book review of: S. B. Cooper (ed.) and J. van Leeuwen (ed.), Alan Turing. His work and impact. (English) Zbl 1338.00010 Notices Am. Math. Soc. 61, No. 8, 886-890 (2014). MSC: 00A17 01-06 01A75 01A60 68-03 03-03 94-03 PDF BibTeX XML Cite \textit{J. Avigad}, Notices Am. Math. Soc. 61, No. 8, 886--890 (2014; Zbl 1338.00010) Full Text: DOI
Avigad, Jeremy Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs. (English) Zbl 1336.00007 Bull. Symb. Log. 20, No. 4, 500-501 (2014). MSC: 00A17 52-01 52C17 PDF BibTeX XML Cite \textit{J. Avigad}, Bull. Symb. Log. 20, No. 4, 500--501 (2014; Zbl 1336.00007) Full Text: DOI
Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody A heuristic prover for real inequalities. (English) Zbl 1416.68149 Klein, Gerwin (ed.) et al., Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 61-76 (2014). MSC: 68T15 68T20 PDF BibTeX XML Cite \textit{J. Avigad} et al., Lect. Notes Comput. Sci. 8558, 61--76 (2014; Zbl 1416.68149) Full Text: DOI
Avigad, Jeremy; Morris, Rebecca The concept of “character” in Dirichlet’s theorem on primes in an arithmetic progression. (English) Zbl 1296.01010 Arch. Hist. Exact Sci. 68, No. 3, 265-326 (2014). Reviewer: Robert W. van der Waall (Huizen) MSC: 01A55 01A60 03-03 00A30 03E20 11-03 11M06 11B25 11N13 30B50 20C15 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{R. Morris}, Arch. Hist. Exact Sci. 68, No. 3, 265--326 (2014; Zbl 1296.01010) Full Text: DOI arXiv
The Univalent Foundations Program [Aczel, Peter; Ahrens, Benedikt; Altenkirch, Thorsten; Awodey, Steve; Barras, Bruno; Bauer, Andrej; Bertot, Yves; Bezem, Marc; Coquand, Thierry; Finster, Eric; Grayson, Daniel; Herbelin, Hugo; Joyal, Andre; Licata, Dan; Lumsdaine, Peter; Mahboubi, Assia; Martin-Lof, Per; Melikhov, Sergey; Pelayo, Alvaro; Polonsky, Andrew; Shulman, Michael; Sozeau, Matthieu; Spitters, Bas; van den Berg, Benno; Voevodsky, Vladimir; Warren, Michael; Zeilberger, Noam; Angiuli, Carlo; Bordg, Anthony; Brunerie, Guillaume; Kapulkin, Chris; Rijke, Egbert; Sojakova, Kristina; Avigad, Jeremy; Cohen, Cyril; Constable, Robert; Curien, Pierre-Louis; Dybjer, Peter; Escardo, Martín; Hou, Kuen-Bang; Gambino, Nicola; Garner, Richard; Gonthier, Georges; Hales, Thomas; Harper, Robert; Hofmann, Martin; Hofstra, Pieter; Kock, Joachim; Kraus, Nicolai; Li, Nuo; Luo, Zhaohui; Nahas, Michael; Palmgren, Erik; Riehl, Emily; Scott, Dana; Scott, Philip; Soloviev, Sergei] Homotopy type theory. Univalent foundations of mathematics. (English) Zbl 1298.03002 Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press. ix, 468 p. (2013). Reviewer: Marco Benini (Buccinasco) MSC: 03-02 55-02 03B15 03G30 18A15 18B05 55U40 PDF BibTeX XML Cite \textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002) Full Text: arXiv Link
Avigad, Jeremy; Iovino, José Ultraproducts and metastability. (English) Zbl 1321.46015 New York J. Math. 19, 713-727 (2013). Reviewer: Manuel González (Santander) MSC: 46B08 03C20 37A30 47A35 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{J. Iovino}, New York J. Math. 19, 713--727 (2013; Zbl 1321.46015) Full Text: arXiv EMIS
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 A machine-checked proof of the odd order theorem. (English) Zbl 1317.68211 Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 163-179 (2013). MSC: 68T15 03B35 20-04 20D10 PDF BibTeX XML Cite \textit{G. Gonthier} et al., Lect. Notes Comput. Sci. 7998, 163--179 (2013; Zbl 1317.68211) Full Text: DOI
Avigad, Jeremy Uniform distribution and algorithmic randomness. (English) Zbl 1275.03133 J. Symb. Log. 78, No. 1, 334-344 (2013). Reviewer: Liang Yu (Nanjing) MSC: 03D32 11K06 PDF BibTeX XML Cite \textit{J. Avigad}, J. Symb. Log. 78, No. 1, 334--344 (2013; Zbl 1275.03133) Full Text: DOI arXiv Euclid Link
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M. \(\delta\)-decidability over the reals. (English) Zbl 1364.03065 Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 305-314 (2012). MSC: 03D78 03B25 03D15 PDF BibTeX XML Cite \textit{S. Gao} et al., in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25--28, 2012. Los Alamitos, CA: IEEE Computer Society. 305--314 (2012; Zbl 1364.03065) Full Text: DOI arXiv
Avigad, Jeremy Type inference in mathematics. (English) Zbl 1267.68207 Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 106, 77-98 (2012). Reviewer: G. E. Mints (Stanford) MSC: 68T15 03F05 03B70 68N15 PDF BibTeX XML Cite \textit{J. Avigad}, Bull. Eur. Assoc. Theor. Comput. Sci. EATCS 106, 77--98 (2012; Zbl 1267.68207) Full Text: arXiv
Avigad, Jeremy; Dean, Edward T.; Rute, Jason A metastable dominated convergence theorem. (English) Zbl 1277.28003 J. Log. Anal. 4, Paper No. 3, 19 p. (2012). MSC: 28A20 03F60 PDF BibTeX XML Cite \textit{J. Avigad} et al., J. Log. Anal. 4, Paper No. 3, 19 p. (2012; Zbl 1277.28003) Full Text: DOI arXiv
Avigad, Jeremy Uncomputably noisy ergodic limits. (English) Zbl 1258.03084 Notre Dame J. Formal Logic 53, No. 3, 347-350 (2012). Reviewer: Douglas Bridges (Christchurch/New Zealand) MSC: 03F60 37A30 PDF BibTeX XML Cite \textit{J. Avigad}, Notre Dame J. Formal Logic 53, No. 3, 347--350 (2012; Zbl 1258.03084) Full Text: DOI arXiv Euclid
Avigad, Jeremy; Dean, Edward T.; Rute, Jason Algorithmic randomness, reverse mathematics, and the dominated convergence theorem. (English) Zbl 1259.03021 Ann. Pure Appl. Logic 163, No. 12, 1854-1864 (2012). Reviewer: Jeffry L. Hirst (Boone) MSC: 03B30 03F35 03D32 03F60 PDF BibTeX XML Cite \textit{J. Avigad} et al., Ann. Pure Appl. Logic 163, No. 12, 1854--1864 (2012; Zbl 1259.03021) Full Text: DOI arXiv
Gao, Sicun; Avigad, Jeremy; Clarke, Edmund M. \(\delta \)-complete decision procedures for satisfiability over the reals. (English) Zbl 1358.03028 Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 286-300 (2012). MSC: 03B35 03B25 PDF BibTeX XML Cite \textit{S. Gao} et al., Lect. Notes Comput. Sci. 7364, 286--300 (2012; Zbl 1358.03028) Full Text: DOI arXiv Link
Avigad, Jeremy Inverting the Furstenberg correspondence. (English) Zbl 1257.37009 Discrete Contin. Dyn. Syst. 32, No. 10, 3421-3431 (2012). Reviewer: Thomas B. Ward (Durham) MSC: 37A45 03F60 PDF BibTeX XML Cite \textit{J. Avigad}, Discrete Contin. Dyn. Syst. 32, No. 10, 3421--3431 (2012; Zbl 1257.37009) Full Text: DOI arXiv
Avigad, Jeremy Understanding, formal verification, and the philosophy of mathematics. (English) Zbl 1273.00032 Gupta, Amitabha (ed.) et al., Logic and philosophy today. Volume 1. London: College Publications (ISBN 978-1-84890-040-0/pbk). Studies in Logic (London) 29, 163-195 (2011). MSC: 00A30 03B35 PDF BibTeX XML Cite \textit{J. Avigad}, Stud. Log. (Lond.) 29, 163--195 (2011; Zbl 1273.00032) Full Text: arXiv
Mancosu, Paolo (ed.) [Giaquinto, Marcus; Manders, Kenneth; Hafner, Johannes; Detlefsen, Michael; Hallett, Michael; Tappenden, Jamie; Avigad, Jeremy; McLarty, Colin; Urquhart, Alasdair] The philosophy of mathematical practice. Paperback edition of the 2008 original. (English) Zbl 1230.03004 Oxford: Oxford University Press (ISBN 978-0-19-964010-2/pbk). xi, 447 p. (2011). MSC: 03-02 03-03 03-06 00A30 01A55 01A60 03A05 18-03 51-03 PDF BibTeX XML Cite \textit{P. Mancosu} (ed.), The philosophy of mathematical practice. Paperback edition of the 2008 original. Oxford: Oxford University Press (2011; Zbl 1230.03004) Full Text: DOI
Asperti, Andrea; Avigad, Jeremy Zen and the art of formalisation. (English) Zbl 1276.03002 Math. Struct. Comput. Sci. 21, No. 4, 679-682 (2011). MSC: 03-03 68-03 03B35 68T15 PDF BibTeX XML Cite \textit{A. Asperti} and \textit{J. Avigad}, Math. Struct. Comput. Sci. 21, No. 4, 679--682 (2011; Zbl 1276.03002) Full Text: DOI
Avigad, Jeremy The computational content of classical arithmetic. (English) Zbl 1244.03153 Feferman, Solomon (ed.) et al., Proofs, categories and computations. Essays in honor of Grigori Mints. With the collaboration of Vladik Kreinovich, Vladimir Lifschitz, and Ruy de Queiroz. London: College Publications (ISBN 978-1-84890-012-7/pbk). Tributes 13, 15-30 (2010). MSC: 03F03 03F30 PDF BibTeX XML Cite \textit{J. Avigad}, Tributes 13, 15--30 (2010; Zbl 1244.03153) Full Text: arXiv
Avigad, Jeremy Gödel and the metamathematical tradition. (English) Zbl 1220.03001 Feferman, Solomon (ed.) et al., Kurt Gödel. Essays for his centennial. Cambridge: Cambridge University Press; Ithaca, NY: Association for Symbolic Logic (ASL) (ISBN 978-0-521-11514-8/hbk). Lecture Notes in Logic 33, 45-60 (2010). Reviewer: Victor V. Pambuccian (Phoenix) MSC: 03-03 03F03 01A60 03A05 PDF BibTeX XML Cite \textit{J. Avigad}, Lect. Notes Log. 33, 45--60 (2010; Zbl 1220.03001)
Avigad, Jeremy; Towsner, Henry Metastability in the Furstenberg-Zimmer tower. (English) Zbl 1230.37004 Fundam. Math. 210, No. 3, 243-268 (2010). Reviewer: Ahmed Hegazi (Mansoura) MSC: 37A05 03F03 03E15 37A25 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{H. Towsner}, Fundam. Math. 210, No. 3, 243--268 (2010; Zbl 1230.37004) Full Text: DOI arXiv
Avigad, Jeremy; Gerhardy, Philipp; Towsner, Henry Local stability of ergodic averages. (English) Zbl 1187.37010 Trans. Am. Math. Soc. 362, No. 1, 261-288 (2010). Reviewer: Athanase Papadopoulos (Strasbourg) MSC: 37A30 03F60 03F03 PDF BibTeX XML Cite \textit{J. Avigad} et al., Trans. Am. Math. Soc. 362, No. 1, 261--288 (2010; Zbl 1187.37010) Full Text: DOI arXiv
Avigad, Jeremy; Dean, Edward; Mumma, John A formal system for Euclid’s Elements. (English) Zbl 1188.03008 Rev. Symb. Log. 2, No. 4, 700-768 (2009). Reviewer: Victor V. Pambuccian (Phoenix) MSC: 03B30 01A20 03B35 03F05 51M05 PDF BibTeX XML Cite \textit{J. Avigad} et al., Rev. Symb. Log. 2, No. 4, 700--768 (2009; Zbl 1188.03008) Full Text: DOI arXiv
Avigad, Jeremy; Towsner, Henry Functional interpretation and inductive definitions. (English) Zbl 1193.03082 J. Symb. Log. 74, No. 4, 1100-1120 (2009). Reviewer: G. E. Mints (Stanford) MSC: 03F10 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{H. Towsner}, J. Symb. Log. 74, No. 4, 1100--1120 (2009; Zbl 1193.03082) Full Text: DOI arXiv
Avigad, Jeremy The metamathematics of ergodic theory. (English) Zbl 1168.03047 Ann. Pure Appl. Logic 157, No. 2-3, 64-76 (2009). Reviewer: Stefano Galatolo (Pisa) MSC: 03F60 37A30 PDF BibTeX XML Cite \textit{J. Avigad}, Ann. Pure Appl. Logic 157, No. 2--3, 64--76 (2009; Zbl 1168.03047) Full Text: DOI
Mancosu, Paolo (ed.) [Giaquinto, Marcus; Manders, Kenneth; Hafner, Johannes; Detlefsen, Michael; Hallett, Michael; Tappenden, Jamie; Avigad, Jeremy; McLarty, Colin; Urquhart, Alasdair] The philosophy of mathematical practice. (English) Zbl 1163.03001 Oxford: Oxford University Press (ISBN 978-0-19-929645-3/hbk). xi, 447 p. (2008). Reviewer: Victor V. Pambuccian (Phoenix) MSC: 03-02 03-03 03-06 00A30 01A55 01A60 03A05 18-03 51-03 PDF BibTeX XML Cite \textit{P. Mancosu} (ed.), The philosophy of mathematical practice. Oxford: Oxford University Press (2008; Zbl 1163.03001)
Avigad, Jeremy; Donnelly, Kevin; Gray, David; Raff, Paul A formally verified proof of the prime number theorem. (English) Zbl 1367.68244 ACM Trans. Comput. Log. 9, No. 1, Article No. 2, 23 p. (2007). MSC: 68T15 03B35 11A41 PDF BibTeX XML Cite \textit{J. Avigad} et al., ACM Trans. Comput. Log. 9, No. 1, Article No. 2, 23 p. (2007; Zbl 1367.68244) Full Text: DOI arXiv
Avigad, Jeremy; Donnelly, Kevin A decision procedure for linear “big O” equations. (English) Zbl 1122.03004 J. Autom. Reasoning 38, No. 4, 353-373 (2007). MSC: 03B25 03B35 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{K. Donnelly}, J. Autom. Reasoning 38, No. 4, 353--373 (2007; Zbl 1122.03004) Full Text: DOI arXiv
Avigad, Jeremy; Yin, Yimu Quantifier elimination for the reals with a predicate for the powers of two. (English) Zbl 1113.03027 Theor. Comput. Sci. 370, No. 1-3, 48-59 (2007). MSC: 03C10 03B25 12L12 68Q25 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{Y. Yin}, Theor. Comput. Sci. 370, No. 1--3, 48--59 (2007; Zbl 1113.03027) Full Text: DOI arXiv
Avigad, Jeremy Methodology and metaphysics in the development of Dedekind’s theory of ideals. (English) Zbl 1164.00001 Ferreirós, José (ed.) et al., The architecture of modern mathematics. Essays in history and philosophy. Oxford: Oxford University Press (ISBN 0-19-856793-6/hbk). 159-186 (2006). Reviewer: Roman Murawski (Poznań) MSC: 00A30 01A55 03A05 16-03 PDF BibTeX XML Cite \textit{J. Avigad}, in: The architecture of modern mathematics. Essays in history and philosophy. Oxford: Oxford University Press. 159--186 (2006; Zbl 1164.00001)
Avigad, Jeremy; Friedman, Harvey Combining decision procedures for the reals. (English) Zbl 1127.03006 Log. Methods Comput. Sci. 2, No. 4, Paper 4, 42 p. (2006). MSC: 03B25 03B35 68T15 68T20 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{H. Friedman}, Log. Methods Comput. Sci. 2, No. 4, Paper 4, 42 p. (2006; Zbl 1127.03006) Full Text: DOI
Avigad, Jeremy Mathematical method and proof. (English) Zbl 1116.03012 Synthese 153, No. 1, 105-159 (2006). Reviewer: Reinhard Kahle (Coimbra) MSC: 03B35 00A30 00A35 03F07 PDF BibTeX XML Cite \textit{J. Avigad}, Synthese 153, No. 1, 105--159 (2006; Zbl 1116.03012) Full Text: DOI Link
Avigad, Jeremy; Simic, Ksenija Fundamental notions of analysis in subsystems of second-order arithmetic. (English) Zbl 1109.03069 Ann. Pure Appl. Logic 139, No. 1-3, 138-184 (2006). Reviewer: Jeffry L. Hirst (Boone) MSC: 03F35 03B30 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{K. Simic}, Ann. Pure Appl. Logic 139, No. 1--3, 138--184 (2006; Zbl 1109.03069) Full Text: DOI
Avigad, Jeremy Weak theories of nonstandard arithmetic and analysis. (English) Zbl 1087.03038 Simpson, Stephen G. (ed.), Reverse mathematics 2001. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic (ASL) (ISBN 1-56881-263-9/hbk; 1-56881-264-7/pbk). Lecture Notes in Logic 21, 19-46 (2005). MSC: 03F35 03H15 PDF BibTeX XML Cite \textit{J. Avigad}, Lect. Notes Log. 21, 19--46 (2005; Zbl 1087.03038)
Avigad, Jeremy; Donnelly, Kevin Formalizing \(O\) notation in Isabelle/HOL. (English) Zbl 1126.68557 Basin, David (ed.) et al., Automated reasoning. Second international joint conference, IJCAR 2004, Cork, Ireland, July 4–8, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22345-2/pbk). Lecture Notes in Computer Science 3097. Lecture Notes in Artificial Intelligence, 357-371 (2004). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{K. Donnelly}, Lect. Notes Comput. Sci. 3097, 357--371 (2004; Zbl 1126.68557) Full Text: DOI
Avigad, Jeremy Forcing in proof theory. (English) Zbl 1064.03034 Bull. Symb. Log. 10, No. 3, 305-333 (2004). MSC: 03F03 03F25 03-02 PDF BibTeX XML Cite \textit{J. Avigad}, Bull. Symb. Log. 10, No. 3, 305--333 (2004; Zbl 1064.03034) Full Text: DOI Link
Avigad, Jeremy Eliminating definitions and Skolem functions in first-order logic. (English) Zbl 1365.03038 ACM Trans. Comput. Log. 4, No. 3, 402-415 (2003). MSC: 03F20 03B10 03F30 PDF BibTeX XML Cite \textit{J. Avigad}, ACM Trans. Comput. Log. 4, No. 3, 402--415 (2003; Zbl 1365.03038) Full Text: DOI Link
Avigad, Jeremy Number theory and elementary arithmetic. (English) Zbl 1050.03005 Philos. Math. (3) 11, No. 3, 257-284 (2003). Reviewer: Andrea Cantini (Firenze) MSC: 03A05 03F30 03F35 00A30 PDF BibTeX XML Cite \textit{J. Avigad}, Philos. Math. (3) 11, No. 3, 257--284 (2003; Zbl 1050.03005) Full Text: DOI Link
Avigad, J.; Helzner, J. Transfer principles in nonstandard intuitionistic arithmetic. (English) Zbl 1024.03068 Arch. Math. Logic 41, No. 6, 581-602 (2002). MSC: 03H15 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{J. Helzner}, Arch. Math. Logic 41, No. 6, 581--602 (2002; Zbl 1024.03068) Full Text: DOI Link
Avigad, Jeremy Saturated models of universal theories. (English) Zbl 1015.03040 Ann. Pure Appl. Logic 118, No. 3, 219-234 (2002); erratum ibid. 121, No. 2-3, 285 (2003). Reviewer: M.Yasuhara (Princeton) MSC: 03C50 03F25 03C25 PDF BibTeX XML Cite \textit{J. Avigad}, Ann. Pure Appl. Logic 118, No. 3, 219--234 (2002; Zbl 1015.03040) Full Text: DOI
Avigad, Jeremy Ordinal analysis without proofs. (English) Zbl 1008.03038 Sieg, Wilfried (ed.) et al., Reflections on the foundations of mathematics. Essays in honor of Solomon Feferman. Natick, MA: A K Peters. Lect. Notes Log. 15, 1-36 (2002). Reviewer: Helmut Pfeiffer (Hannover) MSC: 03F15 03F30 03F05 03F35 03C62 PDF BibTeX XML Cite \textit{J. Avigad}, Lect. Notes Log. 15, 1--36 (2002; Zbl 1008.03038)
Avigad, Jeremy An ordinal analysis of admissible set theory using recursion on ordinal notations. (English) Zbl 1016.03060 J. Math. Log. 2, No. 1, 91-112 (2002). Reviewer: Helmut Pfeiffer (Hannover) MSC: 03F15 03E70 03C70 PDF BibTeX XML Cite \textit{J. Avigad}, J. Math. Log. 2, No. 1, 91--112 (2002; Zbl 1016.03060) Full Text: DOI
Avigad, Jeremy Update procedures and the 1-consistency of arithmetic. (English) Zbl 0988.03087 Math. Log. Q. 48, No. 1, 3-13 (2002). MSC: 03F30 03F10 03F15 03F25 PDF BibTeX XML Cite \textit{J. Avigad}, Math. Log. Q. 48, No. 1, 3--13 (2002; Zbl 0988.03087) Full Text: DOI
Avigad, Jeremy Algebraic proofs of cut elimination. (English) Zbl 1015.68174 J. Log. Algebr. Program. 49, No. 1-2, 15-30 (2001). MSC: 68T15 PDF BibTeX XML Cite \textit{J. Avigad}, J. Log. Algebr. Program. 49, No. 1--2, 15--30 (2001; Zbl 1015.68174) Full Text: DOI
Avigad, Jeremy Interpreting classical theories in constructive ones. (English) Zbl 0981.03061 J. Symb. Log. 65, No. 4, 1785-1812 (2000). Reviewer: Anton Setzer (Uppsala) MSC: 03F50 03F25 03F03 PDF BibTeX XML Cite \textit{J. Avigad}, J. Symb. Log. 65, No. 4, 1785--1812 (2000; Zbl 0981.03061) Full Text: DOI
Avigad, Jeremy A realizability interpretation for classical arithmetic. (English) Zbl 0946.03071 Buss, Samuel R. (ed.) et al., Logic colloquium ’98. Proceedings of the annual European summer meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9-15, 1998. Natick, MA: A K Peters, Ltd. Lect. Notes Log. 13, 57-90 (2000). Reviewer: Andrea Cantini (Firenze) MSC: 03F30 03F50 03F05 03F10 PDF BibTeX XML Cite \textit{J. Avigad}, Lect. Notes Log. 13, 57--90 (2000; Zbl 0946.03071)
Avigad, Jeremy; Sommer, Richard The model-theoretic ordinal analysis of theories of predicative strength. (English) Zbl 0939.03066 J. Symb. Log. 64, No. 1, 327-349 (1999). Reviewer: M.Yasuhara (Princeton) MSC: 03F35 03F15 03C62 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{R. Sommer}, J. Symb. Log. 64, No. 1, 327--349 (1999; Zbl 0939.03066) Full Text: DOI
Avigad, Jeremy Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\). (English) Zbl 0945.03084 Ann. Pure Appl. Logic 92, No. 1, 1-34 (1998). Reviewer: G.Mints (Stanford) MSC: 03F10 03F25 03F30 03F15 PDF BibTeX XML Cite \textit{J. Avigad}, Ann. Pure Appl. Logic 92, No. 1, 1--34 (1998; Zbl 0945.03084) Full Text: DOI
Avigad, Jeremy; Feferman, Solomon Gödel’s functional (“Dialectica”) interpretation. (English) Zbl 0913.03053 Buss, Samuel R. (ed.), Handbook of proof theory. Amsterdam: Elsevier. Stud. Logic Found. Math. 137, 337-405 (1998). Reviewer: A.Cantini (Firenze) MSC: 03F30 03-02 03F35 03F55 03F50 03F60 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{S. Feferman}, Stud. Logic Found. Math. 137, 337--405 (1998; Zbl 0913.03053)
Avigad, Jeremy An effective proof that open sets are Ramsey. (English) Zbl 0909.03040 Arch. Math. Logic 37, No. 4, 235-240 (1998). Reviewer: Benjamin Blankertz (Münster) MSC: 03E05 03F35 PDF BibTeX XML Cite \textit{J. Avigad}, Arch. Math. Logic 37, No. 4, 235--240 (1998; Zbl 0909.03040) Full Text: DOI
Avigad, Jeremy Plausibly hard combinatorial tautologies. (English) Zbl 0891.03024 Beame, Paul W. (ed.) et al., Proof complexity and feasible arithmetics. Papers from the DIMACS workshop, Rutgers, NJ, USA, April 21–24, 1996. Providence, RI: American Mathematical Society. DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 1-12 (1998). MSC: 03F20 68Q15 68Q25 03D15 03B05 PDF BibTeX XML Cite \textit{J. Avigad}, DIMACS, Ser. Discrete Math. Theor. Comput. Sci. 39, 1--12 (1998; Zbl 0891.03024)
Avigad, Jeremy; Sommer, Richard A model-theoretic approach to ordinal analysis. (English) Zbl 0874.03068 Bull. Symb. Log. 3, No. 1, 17-52 (1997). Reviewer: M.Yasuhara (Princeton) MSC: 03F35 03F30 03F15 03C62 03H15 PDF BibTeX XML Cite \textit{J. Avigad} and \textit{R. Sommer}, Bull. Symb. Log. 3, No. 1, 17--52 (1997; Zbl 0874.03068) Full Text: DOI Link Backlinks: MO
Avigad, Jeremy Formalizing forcing arguments in subsystems of second-order arithmetic. (English) Zbl 0860.03040 Ann. Pure Appl. Logic 82, No. 2, 165-191 (1996). Reviewer: R.Murawski (Poznań) MSC: 03F35 03C25 PDF BibTeX XML Cite \textit{J. Avigad}, Ann. Pure Appl. Logic 82, No. 2, 165--191 (1996; Zbl 0860.03040) Full Text: DOI
Avigad, Jeremy On the relationship between \(ATR_ 0\) and \(\widehat {ID}_{<\omega}\). (English) Zbl 0858.03052 J. Symb. Log. 61, No. 3, 768-779 (1996). MSC: 03F15 03F30 03F35 PDF BibTeX XML Cite \textit{J. Avigad}, J. Symb. Log. 61, No. 3, 768--779 (1996; Zbl 0858.03052) Full Text: DOI