zbMATH — the first resource for mathematics

Big math and the one-brain barrier: the tetrapod model of mathematical knowledge. (English) Zbl 07334984
68Vxx Computer science support for mathematical research and practice
Full Text: DOI
[1] AITP: Conference on artificial intelligence and theorem proving. Available at http://aitp-conference.org/.
[2] Kenneth Appel and Wolfgang Haken. Every Planar Map Is Four Colorable, Contemporary Mathematics 98. American Mathematical Society, 1989. · Zbl 0681.05027
[3] Ron Ausbrooks, Stephen Buswell, David Carlisle, et al. Mathematical Markup Language (MathML) version 3.0. W3C Recommendation, World Wide Web Consortium (W3C), 2010.
[4] Katja Berčič. Math databases wiki. Available at https://github.com/MathHubInfo/Documentation/wiki/Math-Databases.
[5] Tim Berners-Lee and Mark Fischetti. Weaving the Web: The Original Design and Ultimate Destiny of the World Wide Web by Its Inventor. Harper, 1999.
[6] Steve Bernstein and Joseph Gelbart, editors. An Introduction to the Langlands Program. Birkhäuser, 2003.
[7] Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science. Springer, 2004. · Zbl 1069.68095
[8] Frederick Brooks. The Mythical Man-Month: Essays on Software Engineering. Addison-Wesley, 1975.
[9] Nicolaas Govert de Bruijn. The mathematical language Automath, its usage and some of its extensions. In Symposium on Automatic Demonstration, Lecture Notes in Mathematics 125, pp. 29-61. Springer, 1970.
[10] Nicolaas Govert de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. In R. P Nederpelt, J. H. Geuvers, and R. C. de Vrijer, editors, Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics 133, pp. 865-935. Elsevier, 1994.
[11] Jacques Carette, William M. Farmer, Yasmine Sharoda, Katja Berčič, Michael Kohlhase, Dennis Müller, and Florian Rabe. The space of mathematical software systems—a survey of paradigmatic systems. Preprint available at http://arxiv.org/abs/2002.04955, 2020.
[12] Corless, RM; Davenport, JH; Jeffrey, DJ; Watt, SM, According to Abramowitz and Stegun, SIGSAM Bulletin, 2, 34, 58-65 (2000)
[13] Joseph Corneli, Ursula Martin, Dave Murray-Rust, Alison Pease, Raymond Puzio, and Gabriela Rino Nesin. Modelling the way mathematics is actually done. In Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, FARM 2017, pp. 10-19. ACM, 2017.
[14] Coq Development Team. The Coq Proof Assistant: Reference Manual. HAL-INRIA. Available at https://hal.inria.fr/inria-00069968.
[15] Cremona, John, The \(L\)-functions and modular forms database project, Foundations of Computational Mathematics, 16, 6, 1541-1553 (2016) · Zbl 1354.11005
[16] Farmer, William M., MKM: A new interdisciplinary field of research, Bulletin of the ACM Special Interest Group on Symbolic and Automated Mathematics (SIGSAM), 38, 2, 47-52 (2004) · Zbl 1341.68225
[17] William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning 11:2 (October 1993), 213-248. · Zbl 0802.68129
[18] The GAP Group. GAP—Groups, Algorithms, and Programming. Available at http://www.gap-system.org, 2016.
[19] G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen, F. Garillot, S. Le Roux, A. Mahboubi, R. O’Connor, et al. A machine-checked proof of the odd order theorem. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, Lecture Notes in Computer Science 7998, pp. 163-179. Springer, 2013. · Zbl 1317.68211
[20] Hales, Thomas C., A Proof of the Kepler Conjecture, Annals of Mathematics, Second Series, 162, 3, 1065-1185 (2005) · Zbl 1096.52010
[21] Thomas Hales. Dense Sphere Packings, London Mathematical Society Lecture Note Series 400. Cambridge University Press, 2012. · Zbl 1263.52001
[22] Hales, Thomas; Adams, Mark; Bauer, Gertrud, A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, 5, E2 (2017) · Zbl 1379.52018
[23] John Harrison. HOL Light: a tutorial introduction. In Proceedings of the First International Conference on Formal Methods in Computer-Aided Design, pp. 265-269. Springer, 1996.
[24] Idris language documentation. Available at http://docs.idris-lang.org/en/latest/.
[25] Donald E. Knuth. Literate Programming. University of Chicago Press, 1992. · Zbl 1109.68387
[26] Kohlhase, Michael; Rabe, Florian, QED reloaded: towards a pluralistic formal library of mathematical knowledge, Journal of Formalized Reasoning, 9, 1, 201-234 (2016) · Zbl 1451.68343
[27] The \(L\)-functions and modular forms database. Available at http://www.lmfdb.org.
[28] Assia Mahboubi and Enrico Tassi. Mathematical components. Available at https://math-comp.github.io/mcb/book.pdf.
[29] Maple: The essential tool for mathematics. Available at https://www.maplesoft.com.
[30] Martin, Ursula, Computational logic and the social, Journal of Logic and Computation, 26, 467-477 (2016) · Zbl 1357.01019
[31] MathOverflow. Available at https://mathoverflow.net.
[32] MathSciNet Mathematical Reviews on the Net. American Mathematical Society. Available at http://www.ams.org/mathscinet/.
[33] Mathworld. Available at http://mathworld.wolfram.com.
[34] Mizar. Available at httpxbpap://www.mizar.org.
[35] MMT: language and system for the uniform representation of knowledge. Project web site at https://uniformal.github.io/.
[36] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25, Lecture Notes in Computer Science 9195, pp. 378-388. Springer, 2015. · Zbl 1465.68279
[37] National Research Council. Developing a 21st Century Global Library for Mathematics Research. The National Academies Press, 2014.
[38] Ulf Norell. The Agda WiKi. Available at http://wiki.portal.chalmers.se/agda.
[39] Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Chalmers University of Technology and Göteborg University, 2007.
[40] Openmath, 2009. Available at http://wiki.openmath.org.
[41] Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, vols. I and II. Elsevier Science and MIT Press, 2001.
[42] PlanetMath.org—math for the people, by the people. Available at http://www.planetmath.org.
[43] Florian Rabe and Michael Kohlhase. A scalable module system. Information & Computation 0.230 (2013), 1-54. · Zbl 1358.68283
[44] Sagemath, the Sage Mathematics Software System. Available at http://www.sagemath.org.
[45] Ronan Saillard. Typechecking in the \(\lambda \Pi \)-Calculus Modulo: Theory and Practice. PhD thesis, École nationale supérieure des mines de Paris, 2015.
[46] Neil, JA, Sloane, The on-line encyclopedia of integer sequences. Notices of the AMS, 50, 8, 912 (2003)
[47] The small groups library. Available at http://www.icm.tu-bs.de/ag_algebra/software/small/small.html.
[48] W3 consortium. webpage at http://www.w3.org. seen February 2007.
[49] Makarius Wenzel. Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In Paolo Masci, Rosemary Monahan, and Virgile Prevosto, editors, F-IDE 2018 - 4th Workshop on Formal Integrated Development Environment, 2018.
[50] Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Ait Mohamed, Munoz, and Tahar, editors, Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science 5170, pp. 33-38. Springer, 2008. · Zbl 1165.68478
[51] Tom Wiesing, Michael Kohlhase, and Florian Rabe. Virtual theories—a uniform interface to mathematical knowledge bases. In Johannes Blömer, Temur Kutsia, and Dimitris Simos, editors, MACIS 2017: Seventh International Conference on Mathematical Aspects of Computer and Information Sciences, Lecture Notes in Computer Science 10693, pp. 243-257. Springer, 2017. · Zbl 07036055
[52] Mark D. Wilkinson, Michel Dumontier, Ijsbrand Aalbersberg, et al. The fair guiding principles for scientific data management and stewardship. Scientific Data, 3 (2016), 160018.
[53] Wolfram Mathematica. Available at https://www.wolfram.com/mathematica/.
[54] zbMATH the first resource in mathematics. Available at http://zbmath.org.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.