{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T18:55:05Z","timestamp":1784314505527,"version":"3.55.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T00:00:00Z","timestamp":1750896000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T00:00:00Z","timestamp":1750896000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["15671644"],"award-info":[{"award-number":["15671644"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>This paper describes a formal theory of smooth vector fields, Lie groups and the Lie algebra of a Lie group in the theorem prover Isabelle. Lie groups are abstract structures that are composable, invertible and differentiable; they are useful in the study of continuous transformations in fields such as particle physics and robotics. The formalisation of this theory in an interactive theorem prover poses challenges beyond those encountered in textbook developments. We comment on representational choices we made to integrate involved concepts, such as smoothness of vector fields, with the simple type theory of higher-order logic (HOL) and existing material in Isabelle\/HOL.<\/jats:p>","DOI":"10.1007\/s10817-025-09724-x","type":"journal-article","created":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T15:28:55Z","timestamp":1750951735000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Constructing the Lie Algebra of Smooth Vector Fields on a Lie Group in Isabelle\/HOL"],"prefix":"10.1007","volume":"69","author":[{"given":"Richard","family":"Schmoetten","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jacques D.","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,6,26]]},"reference":[{"key":"9724_CR1","unstructured":"Adelsberger, S., Hetzl, S., Pollak, F.: The Cayley-Hamilton theorem. Archive of Formal Proofs (2014). https:\/\/isa-afp.org\/entries\/Cayley_Hamilton.html"},{"issue":"2","key":"9724_CR2","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"issue":"6","key":"9724_CR3","doi-asserted-by":"publisher","first-page":"1093","DOI":"10.1007\/s10817-019-09537-9","volume":"64","author":"C Ballarin","year":"2020","unstructured":"Ballarin, C.: Exploring the structure of an algebra text with locales. J. Autom. Reason. 64(6), 1093\u20131121 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09537-9","journal-title":"J. Autom. Reason."},{"key":"9724_CR4","unstructured":"Bordg, A., Cavalleri, N.: Elements of Differential Geometry in Lean: A Report for Mathematicians. arXiv (2021). http:\/\/arxiv.org\/abs\/2108.00484 Accessed 28 Feb 2024"},{"issue":"2","key":"9724_CR5","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1080\/10586458.2022.2062073","volume":"31","author":"A Bordg","year":"2022","unstructured":"Bordg, A., Paulson, L., Li, W.: Simple type theory is not too simple: Grothendieck\u2019s schemes without dependent types. Exp. Math. 31(2), 364\u2013382 (2022). https:\/\/doi.org\/10.1080\/10586458.2022.2062073","journal-title":"Exp. Math."},{"issue":"2","key":"9724_CR6","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1080\/10586458.2021.19834892101.02602","volume":"31","author":"K Buzzard","year":"2022","unstructured":"Buzzard, K., Hughes, C., Lau, K., Livingston, A., Mir, R.F., Morrison, S.: Schemes in lean. Exp. Math. 31(2), 355\u2013363 (2022). https:\/\/doi.org\/10.1080\/10586458.2021.19834892101.02602","journal-title":"Exp. Math."},{"key":"9724_CR7","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25. Lecture Notes in Computer Science","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.) Automated Deduction - CADE-25. Lecture Notes in Computer Science, pp. 378\u2013388. Springer, Cham (2015)"},{"issue":"4","key":"9724_CR8","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.1007\/s10817-022-09631-5","volume":"66","author":"J Divas\u00f3n","year":"2022","unstructured":"Divas\u00f3n, J., Thiemann, R.: A formalization of the Smith normal form in higher-order logic. J. Autom. Reason. 66(4), 1065\u20131095 (2022). https:\/\/doi.org\/10.1007\/s10817-022-09631-5","journal-title":"J. Autom. Reason."},{"key":"9724_CR9","first-page":"236","volume-title":"Automated Reasoning. Lecture Notes in Computer Science","author":"W Guttmann","year":"2020","unstructured":"Guttmann, W.: Reasoning about algebraic structures with implicit carriers in Isabelle\/HOL. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning. Lecture Notes in Computer Science, pp. 236\u2013253. Springer, Cham (2020)"},{"key":"9724_CR10","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, pp. 160\u2013174. Springer, Berlin (2007)"},{"issue":"2","key":"9724_CR11","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reason. 50(2), 173\u2013190 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9250-9","journal-title":"J. Autom. Reason."},{"key":"9724_CR12","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving. Lecture Notes in Computer Science","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, pp. 279\u2013294. Springer, Berlin (2013)"},{"key":"9724_CR13","volume-title":"Certified Programs and Proofs. Lecture Notes in Computer Science","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs. Lecture Notes in Computer Science. Springer, Cham (2013)"},{"key":"9724_CR14","doi-asserted-by":"crossref","unstructured":"Immler, F., Zhan, B.: Smooth manifolds and types to sets for linear algebra in Isabelle\/HOL. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs And Proofs. CPP 2019, pp. 65\u201377. Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3293880.3294093","DOI":"10.1145\/3293880.3294093"},{"key":"9724_CR15","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics Lecture Notes in Computer Science","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics Lecture Notes in Computer Science, pp. 149\u2013165. Springer, Berlin (1999)"},{"key":"9724_CR16","unstructured":"Kappelmann, K.: Transport via Partial Galois Connections and Equivalences. arXiv (2023). http:\/\/arxiv.org\/abs\/2303.05244 Accessed 09 June 2023"},{"key":"9724_CR17","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-319-43144-4_13","volume-title":"Interactive Theorem Proving","author":"O Kun\u010dar","year":"2016","unstructured":"Kun\u010dar, O., Popescu, A.: From types to sets by local type definitions in higher-order logic. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving, vol. 9807, pp. 200\u2013218. Springer, Cham (2016)"},{"key":"9724_CR18","doi-asserted-by":"crossref","unstructured":"Lee, J.M.: Introduction to smooth manifolds. Graduate Texts in Mathematics, vol. 218. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4419-9982-5","DOI":"10.1007\/978-1-4419-9982-5"},{"key":"9724_CR19","unstructured":"Macbeth, H.: Algorithm and Abstraction in Formal Mathematics. arXiv (2024). http:\/\/arxiv.org\/abs\/2405.04699 Accessed 21 Nov 2024"},{"key":"9724_CR20","doi-asserted-by":"crossref","unstructured":"Milehins, M.: An extension of the framework types-to-sets for Isabelle\/HOL. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs And Proofs. CPP 2022, pp. 180\u2013196. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503674","DOI":"10.1145\/3497775.3503674"},{"key":"9724_CR21","doi-asserted-by":"crossref","unstructured":"Nash, O.: Formalising lie algebras. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs And Proofs. CPP 2022, pp. 239\u2013250. Association for Computing Machinery, New York, NY, USA (2022). https:\/\/doi.org\/10.1145\/3497775.3503672","DOI":"10.1145\/3497775.3503672"},{"issue":"3","key":"9724_CR22","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"LC Paulson","year":"1989","unstructured":"Paulson, L.C.: The foundation of a generic theorem prover. J. Autom. Reason. 5(3), 363\u2013397 (1989). https:\/\/doi.org\/10.1007\/BF00248324","journal-title":"J. Autom. Reason."},{"key":"9724_CR23","first-page":"246","volume-title":"COLOG-88. Lecture Notes in Computer Science","author":"LC Paulson","year":"1990","unstructured":"Paulson, L.C.: A formulation of the simple theory of types (for Isabelle). In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG-88. Lecture Notes in Computer Science, pp. 246\u2013274. Springer, Berlin (1990)"},{"key":"9724_CR24","doi-asserted-by":"crossref","unstructured":"Schottenloher, M.: A mathematical introduction to conformal field theory. Lecture Notes in Physics, vol. 759, 2nd edn. Springer, Berlin, Heidelberg (2008)","DOI":"10.1007\/978-3-540-68628-6"},{"key":"9724_CR25","unstructured":"Schmoetten, R., Fleuriot, J.D.: Lie groups and algebras. Archive of Formal Proofs (2024). https:\/\/isa-afp.org\/entries\/Lie_Groups.html, Formal proof development"},{"key":"9724_CR26","volume-title":"A Comprehensive Introduction to Differential Geometry","author":"M Spivak","year":"1999","unstructured":"Spivak, M.: A Comprehensive Introduction to Differential Geometry, vol. 1. Publish or Perish Inc., Houston (1999)"},{"key":"9724_CR27","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511616532","volume-title":"Relativity: An Introduction to Special and General Relativity","author":"H Stephani","year":"2004","unstructured":"Stephani, H.: Relativity: An Introduction to Special and General Relativity. Cambridge University Press, Cambridge (2004)"},{"key":"9724_CR28","unstructured":"Tao, T.: Hilbert\u2019s fifth problem and related topics. Graduate Studies in Mathematics, vol. 153. AMS, ??? (2014). https:\/\/terrytao.wordpress.com\/wp-content\/uploads\/2014\/11\/gsm-153.pdf"},{"key":"9724_CR29","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual. https:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf"},{"key":"9724_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-64612-1","volume-title":"Quantum Theory, Groups and Representations","author":"P Woit","year":"2017","unstructured":"Woit, P.: Quantum Theory, Groups and Representations. Springer, Cham (2017)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09724-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09724-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09724-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:33Z","timestamp":1758664953000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09724-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,26]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9724"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09724-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,26]]},"assertion":[{"value":"25 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 March 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"18"}}