{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:01Z","timestamp":1767927661371,"version":"3.49.0"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T00:00:00Z","timestamp":1733961600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T00:00:00Z","timestamp":1733961600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"crossref","award":["016.Vidi.189.037, Lean Forward"],"award-info":[{"award-number":["016.Vidi.189.037, Lean Forward"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The Lean mathematical library Mathlib features extensive use of the typeclass pattern for organising mathematical structures, based on Lean\u2019s mechanism of instance parameters. Related mechanisms for typeclasses are available in other provers including Agda, Coq and Isabelle with varying degrees of adoption. This paper analyses representative examples of design patterns involving instance parameters in the finalized Lean 3 version of Mathlib, focussing on complications arising at scale and how the Mathlib community deals with them.<\/jats:p>","DOI":"10.1007\/s10817-024-09712-7","type":"journal-article","created":{"date-parts":[[2024,12,12]],"date-time":"2024-12-12T08:37:34Z","timestamp":1733992654000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Use and Abuse of Instance Parameters in the Lean Mathematical Library"],"prefix":"10.1007","volume":"69","author":[{"given":"Anne","family":"Baanen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,12,12]]},"reference":[{"key":"9712_CR1","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-51054-1_1","volume-title":"IJCAR 2020","author":"R Affeldt","year":"2020","unstructured":"Affeldt, R., Cohen, C., Kerjean, M., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS, vol. 12167, pp. 3\u201320. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_1"},{"key":"9712_CR2","unstructured":"Allamigeon, X., Canu, Q., Cohen, C., Sakaguchi, K., Strub, P.-Y.: Design patterns of hierarchies for order structures. ITP 2023, Version 1 (February 2023) (Submitted) (2023). https:\/\/hal.inria.fr\/hal-04008820"},{"key":"9712_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"TPHOLs 2009","author":"A Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 84\u201398. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_8"},{"key":"9712_CR4","doi-asserted-by":"publisher","unstructured":"Baanen, T.: Use and abuse of instance parameters in the Lean mathematical library. In: Andronick, J., Moura, L. (eds.) ITP 2022. LIPIcs, vol. 237, pp. 4\u20131420. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.4","DOI":"10.4230\/LIPIcs.ITP.2022.4"},{"issue":"2","key":"9712_CR5","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":"9712_CR6","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."},{"issue":"5","key":"9712_CR7","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"EC Brady","year":"2013","unstructured":"Brady, E.C.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23(5), 552\u2013593 (2013). https:\/\/doi.org\/10.1017\/S095679681300018X","journal-title":"J. Funct. Program."},{"key":"9712_CR8","doi-asserted-by":"publisher","unstructured":"Buzzard, K., Commelin, J., Massot, P.: Formalising perfectoid spaces. In: CPP \u201920. Certified programs and proofs, pp. 299\u2013312. ACM, New York (2020). https:\/\/doi.org\/10.1145\/3372885.3373830","DOI":"10.1145\/3372885.3373830"},{"key":"9712_CR9","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"34","DOI":"10.4230\/LIPIcs.FSCD.2020.34","volume-title":"FSCD 2020","author":"C Cohen","year":"2020","unstructured":"Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy builder: algebraic hierarchies made easy in Coq with ELPI (system description). In: Ariola, Z.M. (ed.) FSCD 2020. LIPIcs, vol. 167, pp. 34\u201313421. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2020). https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2020.34"},{"key":"9712_CR10","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/3437992.3439919","volume-title":"CPP \u201921. Certified Programs and Proofs","author":"J Commelin","year":"2021","unstructured":"Commelin, J., Lewis, R.Y.: Formalizing the ring of Witt vectors. In: Hri\u021bcu, C., Popescu, A. (eds.) CPP \u201921. Certified Programs and Proofs, pp. 264\u2013277. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3437992.3439919"},{"issue":"9","key":"9712_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/2034574.2034796","volume":"46","author":"D Devriese","year":"2011","unstructured":"Devriese, D., Piessens, F.: On the bright side of type classes: instance arguments in Agda. SIGPLAN Not. 46(9), 143\u2013155 (2011). https:\/\/doi.org\/10.1145\/2034574.2034796","journal-title":"SIGPLAN Not."},{"key":"9712_CR12","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-030-53518-6_16","volume-title":"CICM 2020","author":"F Doorn","year":"2020","unstructured":"Doorn, F., Ebner, G., Lewis, R.Y.: Maintaining a library of formal mathematics. In: Benzm\u00fcller, C., Miller, B.R. (eds.) CICM 2020. LNCS, vol. 12236, pp. 251\u2013267. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_16"},{"key":"9712_CR13","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"TPHOLs 2009","author":"F Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 327\u2013342. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23"},{"key":"9712_CR14","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-642-32347-8_25","volume-title":"ITP 2012","author":"G Gonthier","year":"2012","unstructured":"Gonthier, G., Tassi, E.: A language of patterns for subterm selection. In: Beringer, L., Felty, A. (eds.) ITP 2012, pp. 361\u2013376. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_25"},{"issue":"4","key":"9712_CR15","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1017\/S0956796813000051","volume":"23","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. J. Funct. Program. 23(4), 357\u2013401 (2013). https:\/\/doi.org\/10.1017\/S0956796813000051","journal-title":"J. Funct. Program."},{"key":"9712_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.15439\/2016F520","volume-title":"FedCSIS 2016. Annals of Computer Science and Information Systems","author":"A Grabowski","year":"2016","unstructured":"Grabowski, A., Kornilowicz, A., Schwarzweller, C.: On algebraic hierarchies in mathematical repository of Mizar. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) FedCSIS 2016. Annals of Computer Science and Information Systems, vol. 8, pp. 363\u2013371. IEEE, New York (2016). https:\/\/doi.org\/10.15439\/2016F520"},{"key":"9712_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"ITP 2013","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.) ITP 2013. LNCS, vol. 7998, pp. 279\u2013294. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_21"},{"key":"9712_CR18","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-46425-5_15","volume-title":"Programming Languages and Systems","author":"MP Jones","year":"2000","unstructured":"Jones, M.P.: Type classes with functional dependencies. In: Smolka, G. (ed.) Programming Languages and Systems, pp. 230\u2013244. Springer, Berlin (2000). https:\/\/doi.org\/10.1007\/3-540-46425-5_15"},{"key":"9712_CR19","unstructured":"Jung, R.: Exponential blowup when using unbundled typeclasses to model algebraic hierarchies (2019). https:\/\/www.ralfj.de\/blog\/2019\/05\/15\/typeclasses-exponential-blowup.html. Accessed 1 Feb 2022"},{"key":"9712_CR20","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"TPHOLs\u201999","author":"F Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales\u2014a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) TPHOLs\u201999. LNCS, vol. 1690, pp. 149\u2013166. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_11"},{"key":"9712_CR21","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4457887","volume-title":"The Mathematical Components Libraries","author":"A Mahboubi","year":"2017","unstructured":"Mahboubi, A., Tassi, E.: The Mathematical Components Libraries. Zenodo, Gen\u00e8ve (2017). https:\/\/doi.org\/10.5281\/zenodo.4457887"},{"key":"9712_CR22","unstructured":"Moura, L., Avigad, J., Kong, S., Roux, C.: Elaboration in dependent type theory. CoRR abs\/1505.04324 (2015) arxiv:1505.04324"},{"key":"9712_CR23","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction\u2014CADE-25","author":"L Moura","year":"2015","unstructured":"Moura, L., Kong, S., Avigad, J., Doorn, F., Raumer, J.: The Lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction\u2014CADE-25. LNCS, vol. 9195, pp. 378\u2013388. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"9712_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction\u2014CADE-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.) Automated Deduction\u2014CADE-28. LNCS, vol. 12699, pp. 625\u2013635. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"issue":"10","key":"9712_CR25","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/1932682.1869489","volume":"45","author":"BCS Oliveira","year":"2010","unstructured":"Oliveira, B.C.S., Moors, A., Odersky, M.: Type classes as objects and implicits. SIGPLAN Not. 45(10), 341\u2013360 (2010). https:\/\/doi.org\/10.1145\/1932682.1869489","journal-title":"SIGPLAN Not."},{"key":"9712_CR26","doi-asserted-by":"publisher","unstructured":"Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1853\u20131964. Elsevier and MIT Press, Amsterdam and Cambridge (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50028-X","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"9712_CR27","doi-asserted-by":"publisher","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: Principles of Programming Languages\u2014POPL \u201997, pp. 292\u2013301. ACM, New York (1997). https:\/\/doi.org\/10.1145\/263699.263742","DOI":"10.1145\/263699.263742"},{"key":"9712_CR28","doi-asserted-by":"publisher","unstructured":"Sakaguchi, K.: Reflexive tactics for algebra, revisited. In: Andronick, J., Moura, L. (eds.) ITP 2022. LIPIcs, vol. 237, pp. 29\u201312922. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022).https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.29","DOI":"10.4230\/LIPIcs.ITP.2022.29"},{"key":"9712_CR29","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-51054-1_8","volume-title":"IJCAR 2020","author":"K Sakaguchi","year":"2020","unstructured":"Sakaguchi, K.: Validating mathematical structures. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS, vol. 12167, pp. 138\u2013157. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_8"},{"key":"9712_CR30","unstructured":"Selsam, D., Ullrich, S., Moura, L.: Tabled typeclass resolution. CoRR (2020). arxiv:2001.04301"},{"key":"9712_CR31","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"TPHOLs 2008","author":"M Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278\u2013293. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23"},{"key":"9712_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/978-3-642-14052-5_35","volume-title":"ITP 2010","author":"B Spitters","year":"2010","unstructured":"Spitters, B., Weegen, E.: Developing the algebraic hierarchy with type classes in Coq. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 490\u2013493. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_35"},{"key":"9712_CR33","doi-asserted-by":"publisher","unstructured":"The mathlib Community: The Lean mathematical library. In: Blanchette, J., Hri\u021bcu, C. (eds.) CPP 2020. Certified Programs and Proofs, pp. 367\u2013381. ACM, New York City, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"9712_CR34","unstructured":"The Rust team: The Rust Reference 1.57.0 (2021). https:\/\/doc.rust-lang.org\/1.57.0\/reference\/index.html. Accessed 22 Dec 2021"},{"key":"9712_CR35","doi-asserted-by":"publisher","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Principles of Programming Languages. POPL \u201989, pp. 60\u201376. ACM, New York (1989). https:\/\/doi.org\/10.1145\/75277.75283","DOI":"10.1145\/75277.75283"},{"key":"9712_CR36","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"TPHOLs\u201997","author":"M Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs\u201997. LNCS, vol. 1275, pp. 307\u2013322. Springer, Berlin (1997). https:\/\/doi.org\/10.1007\/BFb0028402"},{"key":"9712_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-3-031-42753-4_15","volume-title":"CICM 2023","author":"E Wieser","year":"2023","unstructured":"Wieser, E.: Multiple-inheritance hazards in dependently-typed algebraic hierarchies. In: Dubois, C., Kerber, M. (eds.) CICM 2023. Lecture Notes in Computer Science, vol. 14101, pp. 222\u2013236. Springer, Berlin (2023). https:\/\/doi.org\/10.1007\/978-3-031-42753-4_15"},{"key":"9712_CR38","unstructured":"Wieser, E.: Scalar actions in Lean\u2019s mathlib. CoRR (2021). arxiv:2108.10700"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09712-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09712-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09712-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:51:00Z","timestamp":1742676660000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09712-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,12]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9712"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09712-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,12]]},"assertion":[{"value":"31 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"26 August 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 December 2024","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 author has 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":"1"}}