## Formalising mathematics – in praxis; a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started.(English)Zbl 07323056

The main goal of the paper is to give an overview of the author’s work experiences with Isabelle/HOL so far and of the author’s views on the formalisation of mathematics, and to share some instructions on getting started with Isabelle as well as some first observations which the author made, both technical and conceptual, that might prove to be helpful to students and beginners in their early learning stages. In particular, the author introduced the ALEXANDRIA project at the University of Cambridge.

### MSC:

 68V20 Formalization of mathematics in connection with theorem provers 03B35 Mechanization of proofs and logical operations 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) 68V35 Digital mathematics libraries and repositories
Full Text:

### References:

 [1] Archive of Formal Proofs: https://www.isa-afp.org. Accessed 2 September 2020 [2] Aristotle; Crisp, R., Nicomachean Ethics (2014), Cambridge: Cambridge University Press, Cambridge [3] Avigad, J., The mechanization of mathematics, Not. Am. Math. Soc., 65, 6, 681-690 (2018) · Zbl 1398.68478 [4] Barendregt, H.; Wiedijk, F., The challenge of computer mathematics, Philos. Trans. - Royal Soc., Math. Phys. Eng. Sci., 363, 1835, 2351-2375 (2005) · Zbl 1152.03304 [5] Blanchette, J. C.; Kaliszyk, C.; Paulson, L. C.; Urban, C., Hammer-ing towards QED, J. Formaliz. Reason., 9, 1, 101-148 (2016) · Zbl 1451.68318 [6] Boyer, R.; Bundy, A., The QED manifesto, Automated Deduction - CADE 12, 238-251 (1994), Berlin: Springer, Berlin [7] Buzzard, K.: The Xena Project: Mathematicians learning Lean by doing (blog). https://xenaproject.wordpress.com. Accessed on 4 September 2020 [8] Buzzard, K.: Computers and mathematics. Newsletter of the London Mathematical Society, Issue 484 (2019) [9] Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces (2019). Submitted preprint, arXiv:1910.12320 [10] Erdős, P.; Straus, E. G., On the irrationality of certain series, Pac. J. Math., 55, 1, 85-92 (1974) · Zbl 0279.10026 [11] Freiberger, M.: Pure Maths in Crisis? +plus magazine. https://plus.maths.org/content/pure-maths-crisis (2019). Submitted on 19 March 2019, accessed on 4 Sept. 2020 [12] Gonthier, G., Formal proof-the Four-Color Theorem, Not. Am. Math. Soc., 55, 11, 1382-1393 (2008) · Zbl 1195.05026 [13] Gouëzel, S.; Shchur, V., A corrected quantitative version of the Morse lemma, J. Funct. Anal., 277, 4, 1258-1268 (2019) · Zbl 1419.53049 [14] Gowers, T.; Alon, N.; Bourgain, J.; Connes, A.; Gromov, M.; Milman, V., Rough structure and classification, Modern Birkhäuser Classics (2010), Basel: Birkhäuser, Basel [15] Gowers, T.: Does Mathematics Need a Philosophy? https://www.dpmms.cam.ac.uk/ wtg10/philosophy.html. Accessed 4 September 2020 · Zbl 1167.00006 [16] Hales, T., A proof of the Kepler conjecture, Ann. Math., 162, 3, 1065-1185 (2005) · Zbl 1096.52010 [17] Hales, T.; Adams, M.; Bauer, G.; Dang, T. D.; Harrison, J.; Hoang, L. T.; Kaliszyk, C.; Magron, V.; McLaughlin, S.; Nguyen, T. T.; Nguyen, Q. T.; Nipkow, T.; Obua, S.; Pleso, J.; Rute, J.; Solovyev, A.; Ta, T. H.A.; Tran, N. T.; Trieu, T. D.; Urban, J.; Vu, K.; Zumkeller, R., A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, e2 (2017) · Zbl 1379.52018 [18] Hančl, J., Irrational Rapidly Convergent Series (2002) · Zbl 1165.40301 [19] Hančl, J.; Rucki, P., The transcendence of certain infinite series, Rocky Mt. J. Math., 35, 2, 531-537 (2005) · Zbl 1092.11033 [20] Huch, F., Krauss, A.: FindFacts: a scalable theorem search. In: Online proceedings of the Isabelle Workshop 2020, affiliated to IJCAR 2020 (in Virtual Space), June 30, 2020. https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_3.pdf [21] Isabelle Website: https://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html. Accessed 4 September 2020 [22] Isabelle/HOL Library: http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/index.html. Accessed 4 September 2020 [23] Isabelle/ZF Library: https://isabelle.in.tum.de/dist/library/ZF/index.html. Accessed 4 September 2020 [24] Koepke, P.; Schröder-Heister, P.; Heinzmann, G.; Hodges, W.; Bour, P. E., Mathematics and the new technologies, part II: computer-assisted formal mathematics and mathematical practice, Logic, Methodology and Philosophy of Science - Proceedings of the 14th International Congress (2014) [25] Kohlenbach, U., Applied Proof Theory: Proof Interpretations and Their Use in Mathematics (2008), Berlin: Springer, Berlin · Zbl 1158.03002 [26] Kohlenbach, U., Recent progress in proof mining in nonlinear analysis, IfCoLog J. Log. Appl., 10, 4, 3361-3410 (2017) [27] Kohlenbach, U.; Sirakov, B.; Ney de Souza, P.; Viana, M., Proof-theoretic methods in nonlinear analysis, Proceedings of the International Congress of Mathematicians 2018, 61-82 (2019), Singapore: World Scientific, Singapore [28] Kohlenbach, U.; Koutsoukou-Argyraki, A., Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators, J. Math. Anal. Appl., 423, 1089-1112 (2015) · Zbl 1300.47070 [29] Kohlenbach, U.; Koutsoukou-Argyraki, A., Effective asymptotic regularity for one-parameter nonexpansive semigroups, J. Math. Anal. Appl., 433, 1883-1903 (2016) · Zbl 1432.03116 [30] Koutsoukou-Argyraki, A., Effective rates of convergence for the resolvents of accretive operators, Numer. Funct. Anal. Optim., 38, 12, 1601-1613 (2017) · Zbl 1491.47052 [31] Koutsoukou-Argyraki, A., New effective bounds for the approximate common fixed points and asymptotic regularity of nonexpansive semigroups, J. Log. Anal., 10:7, 1-30 (2018) · Zbl 06983477 [32] Koutsoukou-Argyraki, A.: Proof Mining for Nonlinear Operator Theory: Four Case Studies on Accretive Operators, the Cauchy Problem and Nonexpansive Semigroups. PhD thesis, TU Darmstadt (2017). URN:urn:nbn:de:tuda-tuprints-61015. https://tuprints.ulb.tu-darmstadt.de/id/eprint/6101 · Zbl 1368.47001 [33] Koutsoukou-Argyraki, A.: Aristotle’s Assertoric Syllogistic. Archive of Formal Proofs (2019). Formal proof development. https://www.isa-afp.org/entries/Aristotles_Assertoric_Syllogistic.html [34] Koutsoukou-Argyraki, A.: Octonions. Archive of Formal Proofs (2018). Formal proof development. https://www.isa-afp.org/entries/Octonions.html · Zbl 1368.47001 [35] Koutsoukou-Argyraki, A.: Amicable Numbers. Archive of Formal Proofs (2020). Formal proof development. https://www.isa-afp.org/entries/Amicable_Numbers.html · Zbl 1368.47001 [36] Koutsoukou-Argyraki, A.: Proof mining mathematics, formalising mathematics. Bull. Symb. Log. 24(4) (2018). Proceedings of the North American Annual Meeting of the Association for Symbolic Logic, University of Western Illinois, Macomb, Illinois, USA, May 16-19, 2018 · Zbl 1368.47001 [37] Koutsoukou-Argyraki, A.: On preserving the computational content of mathematical proofs: toy examples for a formalising strategy. In preparation · Zbl 1491.47052 [38] Koutsoukou-Argyraki, A., Li, W.: Irrational rapidly convergent series. Archive of Formal Proofs (2018). Formal proof development. https://www.isa-afp.org/entries/Irrationality_J_Hancl.html [39] Koutsoukou-Argyraki, A., Li, W.: The transcendence of certain infinite series. Archive of Formal Proofs (2019). Formal proof development. https://www.isa-afp.org/entries/Transcendence_Series_Hancl_Rucki.html [40] Koutsoukou-Argyraki, A., Li, W.: Irrationality Criteria for Series by Erdős and Straus. Archive of Formal Proofs (2020). Formal proof development. https://www.isa-afp.org/entries/Irrational_Series_Erdos_Straus.html [41] Lakatos, I.; Worrall, J.; Zahar, E., Proofs and Refutations (1976), Cambridge: Cambridge University Press, Cambridge [42] Lamport, L., How to write a 21st century proof, J. Fixed Point Theory Appl., 11, 43 (2012) · Zbl 1271.03082 [43] Löwe, B.; Schröder-Heister, P.; Heinzmann, G.; Hodges, W.; Bour, P. E., Mathematics and the new technologies, part I: philosophical relevance of a changing culture of mathematics, Logic, Methodology and Philosophy of Science - Proceedings of the 14th International Congress (2014) [44] The MathOverflow Community: Nonequivalent definitions in Mathematics, Question asked by Koutsoukou-Argyraki, A. on 22 Nov. 2017. https://mathoverflow.net/questions/286732/nonequivalent-definitions-in-mathematics [45] Negri, S.; Plato, J. V., Proof Analysis-A Contribution to Hilbert’s Last Problem (2011), Cambridge: Cambridge University Press, Cambridge · Zbl 1247.03001 [46] Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Berlin: Springer, Berlin · Zbl 0994.68131 [47] Paulson, L.C.: ALEXANDRIA: Large-scale formal proof for the working mathematician. Project description (12 Nov. 2018). http://www.cl.cam.ac.uk/ lp15/Grants/Alexandria/ [48] Paulson, L. C., A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets, Rev. Symb. Log., 7, 3, 484-498 (2013) · Zbl 1337.03021 [49] Paulson, L. C., A mechanised proof of Gödel’s incompleteness theorems using nominal Isabelle, J. Autom. Reason., 55, 1-37 (2015) · Zbl 1357.68200 [50] Paulson, L. C., Computational logic: its origins and applications, Proc. R. Soc. A, Math. Phys. Eng. Sci., 474, 2210 (2018) · Zbl 1402.68160 [51] Paulson, L. C., The foundation of a generic theorem prover, J. Autom. Reason., 5, 3, 363-397 (1989) · Zbl 0679.68173 [52] Paulson, L.C.: Quaternions. Archive of Formal Proofs (2018). Formal proof development. https://www.isa-afp.org/entries/Quaternions.html [53] Paulson, L. C.; Sarikaya, D.; Kant, D.; Centrone, S., Formalising mathematics in simple type theory, Reflections on the Foundations of Mathematics (2019), Berlin: Springer, Berlin [54] Pöppe, C.: Hilbert und Isabelle. Spektrum.de. 20.02.2019 (in German). https://www.spektrum.de/magazin/optimierung-diophantischer-gleichungen/1621174?utm_medium=newsletter&utm_source=sdw-nl&utm_campaign=sdw-nl-mag [55] Roth, K. F., Rational approximations to algebraic numbers, Mathematica, 2, 3, 1-20 (1955) · Zbl 0064.28501 [56] Russell, S.; Norvig, P., Artificial Intelligence: A Modern Approach (2010) · Zbl 0835.68093 [57] Smith, R.: Aristotle’s Logic. The Stanford Encyclopedia of Philosophy (website). First published 18 March 2000. Substantive revision 17 February 2017. https://plato.stanford.edu/entries/aristotle-logic/ [58] Stock, B., et al.: Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle. EasyChair Preprint No. 152, EasyChair (2018). doi:10.29007/3q4s [59] Stathopoulos, Y., Koutsoukou-Argyraki, A., Paulson, L.C.: SErAPIS: A Concept-Oriented Search Engine for the Isabelle Libraries Based on Natural Language. In: Online proceedings of the Isabelle Workshop 2020 affiliated to IJCAR 2020 (in Virtual Space), June 30, 2020. https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_4.pdf [60] Stathopoulos, Y., Koutsoukou-Argyraki, A., Paulson, L.C.: Developing a Concept-Oriented Search Engine for Isabelle Based on Natural Language: Technical Challenges. In: Online proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving (AITP 2020), Aussois, France, March 22-27 (event postponed to September 13-18, 2020). http://aitp-conference.org/2020/abstract/paper_9.pdf [61] Voevodsky, V.: The Origins and Motivations of Univalent Foundations. The Institute Letter, Institute of Advanced Studies (2014). https://www.ias.edu/sites/default/files/pdfs/publications/letter-2014-summer.pdf [62] Whitehead, A. N.; Russell, B., Principia Mathematica (1927), Cambridge: Cambridge University Press, Cambridge · JFM 61.0061.03 [63] Wiedijk, F., The De Bruijn Factor (2000) [64] Wiedijk, F.: The De Bruijn Factor (Webpage). http://www.cs.ru.nl/ freek/factor/. Accessed on 4 September 2020 [65] Wiedijk, F., The Seventeen Provers of the World, forward by Dana S. Scott (2006), Berlin: Springer, Berlin · Zbl 1084.68119 [66] Wiedijk, F.: Formalizing 100 Theorems (Webpage). http://www.cs.ru.nl/ freek/100/. Accessed 4 September 2020 [67] Wimmer, S., Noschinski, L.: Pratt’s Primality Certificates. Archive of Formal Proofs (2013). Formal proof development. https://www.isa-afp.org/entries/Pratt_Certificate.html [68] Wittgenstein, L., Tractatus Logico-Philosophicus (Logisch-Philosophische Abhandlung), W. Ostwald’s Annalen der Naturphilosophie (1921) · Zbl 0117.25106
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.