{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T14:30:31Z","timestamp":1742999431698,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031645280"},{"type":"electronic","value":"9783031645297"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-64529-7_2","type":"book-chapter","created":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T15:21:35Z","timestamp":1721143295000},"page":"12-25","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Algorithm and\u00a0Abstraction in\u00a0Formal Mathematics"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0290-4172","authenticated-orcid":false,"given":"Heather","family":"Macbeth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,17]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-51054-1_1","volume-title":"Automated Reasoning","author":"R Affeldt","year":"2020","unstructured":"Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in\u00a0dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 3\u201320. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_1"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1070\/RM1998v053n01ABEH000005","volume":"53","author":"VI Arnold","year":"1998","unstructured":"Arnold, V.I.: On teaching mathematics. Russ. Math. Surv. 53(1), 229\u2013236 (1998). https:\/\/doi.org\/10.1070\/RM1998v053n01ABEH000005","journal-title":"Russ. Math. Surv."},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formal proof of the Lax-Milgram theorem. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp. 79\u201389. Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3018610.3018625","DOI":"10.1145\/3018610.3018625"},{"issue":"1","key":"2_CR4","doi-asserted-by":"publisher","first-page":"8","DOI":"10.2307\/2320989","volume":"89","author":"FF Bonsall","year":"1982","unstructured":"Bonsall, F.F.: A down-to-earth view of mathematics. Am. Math. Mon. 89(1), 8\u201315 (1982). https:\/\/doi.org\/10.2307\/2320989","journal-title":"Am. Math. Mon."},{"issue":"4","key":"2_CR5","doi-asserted-by":"publisher","first-page":"221","DOI":"10.2307\/2305937","volume":"57","author":"N Bourbaki","year":"1950","unstructured":"Bourbaki, N.: The architecture of mathematics. Am. Math. Mon. 57(4), 221\u2013232 (1950). https:\/\/doi.org\/10.2307\/2305937","journal-title":"Am. Math. Mon."},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-540-73086-6_3","volume-title":"Towards Mechanized Mathematical Assistants","author":"A Chaieb","year":"2007","unstructured":"Chaieb, A., Wenzel, M.: Context aware calculation and deduction. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM -2007. LNCS (LNAI), vol. 4573, pp. 27\u201339. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73086-6_3"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1090\/bull\/1831","volume":"61","author":"J Commelin","year":"2024","unstructured":"Commelin, J., Topaz, A.: Abstraction boundaries and spec driven development in pure mathematics. Bull. Am. Math. Soc. 61(2), 241\u2013255 (2024). https:\/\/doi.org\/10.1090\/bull\/1831","journal-title":"Bull. Am. Math. Soc."},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"mathlib community, T.: The Lean mathematical library. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367\u2013381. Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Conway, J.H., Burgiel, H., Goodman-Strauss, C.: The Symmetries of Things, A K Peters, Wellesley, MA (2008). https:\/\/doi.org\/10.1201\/b21368","DOI":"10.1201\/b21368"},{"key":"2_CR10","unstructured":"Eck, D.: Wallpaper symmetry sketchpad. https:\/\/math.hws.edu\/eck\/js\/symmetry\/wallpaper.html. Accessed 25 March 2024"},{"key":"2_CR11","unstructured":"Gonthier, G.: Formal proof - the four color theorem. Notices Am. Math. Soc. 55(11), 1382\u20131393 (2008). www.ams.org\/notices\/200811\/tx081101382p.pdf"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-16681-5_1","volume-title":"Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19\u201323, 2022, Proceedings","author":"S Gou\u00ebzel","year":"2022","unstructured":"Gou\u00ebzel, S.: A formalization of\u00a0the\u00a0change of\u00a0variables formula for\u00a0integrals in\u00a0mathlib. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics: 15th International Conference, CICM 2022, Tbilisi, Georgia, September 19\u201323, 2022, Proceedings, pp. 3\u201318. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_1"},{"key":"2_CR14","doi-asserted-by":"publisher","first-page":"e2","DOI":"10.1017\/fmp.2017.1","volume":"5","author":"T Hales","year":"2017","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. Forum Math. Pi 5, e2 (2017). https:\/\/doi.org\/10.1017\/fmp.2017.1","journal-title":"Forum Math. Pi"},{"issue":"16","key":"2_CR15","first-page":"123","volume":"2","author":"PR Halmos","year":"1970","unstructured":"Halmos, P.R.: How to write mathematics. Enseign. Math. 2(16), 123\u2013152 (1970)","journal-title":"Enseign. Math."},{"key":"2_CR16","unstructured":"Hardy, G.H.: A mathematician\u2019s apology. Cambridge University Press (1940)"},{"key":"2_CR17","unstructured":"Harrison, J.: Formalized mathematics. Technical Report\u00a036, Turku Centre for Computer Science (TUCS), Lemmink\u00e4isenkatu 14 A, FIN-20520 Turku, Finland (1996). http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/form-math3.html"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-73595-3_5","volume-title":"Automated Deduction \u2013 CADE-21","author":"J Harrison","year":"2007","unstructured":"Harrison, J.: Automating elementary number-theoretic proofs using Gr\u00f6bner bases. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 51\u201366. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_5"},{"key":"2_CR19","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/s10817-009-9145-6","volume":"43","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Formalizing an analytic proof of the prime number theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reason. 43, 243\u2013261 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9145-6","journal-title":"J. Autom. Reason."},{"key":"2_CR20","unstructured":"Howard, P.: Lecture notes for M612: Partial Differential Equations (2020). https:\/\/people.tamu.edu\/~phoward\/M612.html"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s10817-017-9448-y","volume":"61","author":"F Immler","year":"2018","unstructured":"Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reason. 61(1), 73\u2013111 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9448-y","journal-title":"J. Autom. Reason."},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Inglis, M., Aberdein, A.: Beauty is not simplicity: an analysis of mathematicians\u2019 proof appraisals. Philosophia Math. 23(1), 87\u2013109 (07 2014). https:\/\/doi.org\/10.1093\/philmat\/nku014","DOI":"10.1093\/philmat\/nku014"},{"key":"2_CR23","unstructured":"Kobayashi, S., Nomizu, K.: Foundations of Differential Geometry, Volume I, Issue 15, Volumes 1-2 of Interscience Tracts in Pure and Applied Mathematics, Interscience Publishers, New York, NY (1963)"},{"issue":"1","key":"2_CR24","first-page":"59","volume":"17","author":"S Kochen","year":"1967","unstructured":"Kochen, S., Specker, E.P.: The problem of hidden variables in quantum mechanics. J. Math. Mech. 17(1), 59\u201387 (1967)","journal-title":"J. Math. Mech."},{"issue":"4","key":"2_CR25","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00283-012-9325-9","volume":"34","author":"U Monta\u00f1o","year":"2012","unstructured":"Monta\u00f1o, U.: Ugly mathematics: why do mathematicians dislike computer-assisted proofs? Math. Intell. 34(4), 21\u201328 (2012). https:\/\/doi.org\/10.1007\/s00283-012-9325-9","journal-title":"Math. Intell."},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"2_CR28","doi-asserted-by":"publisher","unstructured":"Peres, A.: Two simple proofs of the Kochen-Specker theorem. J. Phys. A Math. Gen. 24(4), l175\u2013l178 (1991). https:\/\/doi.org\/10.1088\/0305-4470\/24\/4\/003","DOI":"10.1088\/0305-4470\/24\/4\/003"},{"key":"2_CR29","unstructured":"Pottier, L.: Connecting Gr\u00f6bner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008. CEUR Workshop Proceedings, vol.\u00a0418, CEUR-WS.org (2008). https:\/\/ceur-ws.org\/Vol-418\/paper5.pdf"},{"issue":"2","key":"2_CR30","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1004930722234","volume":"111","author":"GC Rota","year":"1997","unstructured":"Rota, G.C.: The phenomenology of mathematical beauty. Synthese 111(2), 171\u2013182 (1997). https:\/\/doi.org\/10.1023\/A:1004930722234","journal-title":"Synthese"},{"key":"2_CR31","doi-asserted-by":"publisher","unstructured":"Tao, T.: What is good mathematics? Bull. Am. Math. Soc. New Ser. 44(4), 623\u2013634 (2007). https:\/\/doi.org\/10.1090\/S0273-0979-07-01168-8","DOI":"10.1090\/S0273-0979-07-01168-8"},{"issue":"3","key":"2_CR32","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/BF03024015","volume":"12","author":"D Wells","year":"1990","unstructured":"Wells, D.: Are these the most beautiful? Math. Intell. 12(3), 37\u201341 (1990). https:\/\/doi.org\/10.1007\/BF03024015","journal-title":"Math. Intell."}],"container-title":["Lecture Notes in Computer Science","Mathematical Software \u2013 ICMS 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-64529-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,16]],"date-time":"2024-07-16T15:22:06Z","timestamp":1721143326000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-64529-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031645280","9783031645297"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-64529-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"17 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The author has no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"ICMS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Congress on Mathematical Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Durham","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icms2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/maths.dur.ac.uk\/icms2024\/ICMS2024.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}