{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T07:22:15Z","timestamp":1769584935847,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T00:00:00Z","timestamp":1759881600000},"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":[[2026]]},"DOI":"10.1007\/978-3-032-07021-0_4","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:40:32Z","timestamp":1759844432000},"page":"51-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Growing Mathlib: maintenance of a large scale mathematical library"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8497-3683","authenticated-orcid":false,"given":"Anne","family":"Baanen","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5819-0159","authenticated-orcid":false,"given":"Matthew Robert","family":"Ballard","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2025-9771","authenticated-orcid":false,"given":"Johan","family":"Commelin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7023-7252","authenticated-orcid":false,"given":"Bryan Gin\u2013ge","family":"Chen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0001-8307-4122","authenticated-orcid":false,"given":"Michael","family":"Rothgang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0004-5949-6861","authenticated-orcid":false,"given":"Damiano","family":"Testa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,8]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Anne Baanen. \u201cUse and Abuse of Instance Parameters in the Lean Mathematical Library\u201d. In: 13th International Conference on Interactive Theorem Proving (ITP 2022). Ed. by June Andronick and Leonardo de Moura. Vol. 237. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2022, 4:1\u20134:20. doi: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.4. url: https:\/\/drops.dagstuhl.de\/pus\/volltexte\/2022\/16713.","DOI":"10.4230\/LIPIcs.ITP.2022.4"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek et al. \u201cThe Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar\u201d. In: Journal of Automated Reasoning 61 (June 2018), pp. 9\u201332. url: https:\/\/link.springer.com\/article\/10.1007\/s10817-017-9440-6.","DOI":"10.1007\/s10817-017-9440-6"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Jasmin Blanchette et al. \u201cMining the Archive of Formal Proofs\u201d. In: Conference on Intelligent Computer Mathematics (CICM 2015). Ed. by M. Kerber. Vol. 9150. LNCS. Invited paper. Springer, 2015, pp. 3\u201317.","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Timothy Bourke et al. \u201cChallenges and Experiences in Managing Large- Scale Proofs\u2019. In: AISC\/MKM\/Calculemus. 2012. url: https:\/\/api.semanticscholar.org\/CorpusID:11296777.","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"4_CR5","unstructured":"Kevin Buzzard. The Fermat\u2019s Last Theorem Project. Lean community blog. Apr. 2024. url: https:\/\/leanprover-community.github.io\/blog\/posts\/FLT-announcement\/."},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Johan Commelin and Adam Topaz. \u201cAbstraction boundaries and spec driven development in pure mathematics\u201d. In: Bull. Amer. Math. Soc. (N.S.) 61.2 (2024), pp. 241\u2013255. doi: https:\/\/doi.org\/10.1090\/bull\/1831. url: https:\/\/doi.org\/10.1090\/bull\/1831.","DOI":"10.1090\/bull\/1831"},{"key":"4_CR7","unstructured":"Mathlib Community. \u201cCompletion of the Liquid Tensor Experiment\u201d. July 2022. url: https:\/\/leanprover-community.github.io\/blog\/posts\/lte-final\/."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Ward Cunningham. The WyCash Portfolio Management System. OOPSLA \u201992 Experience report. Mar. 1992. url: https:\/\/c2.com\/doc\/oopsla92.html.","DOI":"10.1145\/157709.157715"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Floris van Doorn, Patrick Massot, and Oliver Nash. \u201cFormalising the h- Principle and Sphere Eversion\u201d. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. Ed. by Robbert Krebbers et al. ACM, 2023, pp. 121\u2013134. doi: https:\/\/doi.org\/10.1145\/3573105.3575688. url: https:\/\/doi.org\/10.1145\/3573105.3575688.","DOI":"10.1145\/3573105.3575688"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Ali Ghanbari. \u201cAutomatic Goal Clone Detection in Rocq\u201d. In: 39th European Conference on Object-Oriented Programming, ECOOP 2025, June 30 to July 2, 2025, Bergen, Norway. Ed. by Jonathan Aldrich and Alexandra Silva. Vol. 333. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2025, 12:1\u201312:19. doi: https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2025.12. url: https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2025.12.","DOI":"10.4230\/LIPICS.ECOOP.2025.12"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. \u201cMostly Automated Proof Repair for Verified Libraries\u201d. In: Proceedings of the ACM on Programming Languages 7 (2023), pp. 25\u201349. url: https:\/\/api.semanticscholar.org\/CorpusID:259091808.","DOI":"10.1145\/3591221"},{"key":"4_CR12","unstructured":"W. T. Gowers et al. \u201cMarton\u2019s Conjecture in abelian groups with bounded torsion\u201d. arXiv:2404.02244 [math.NT]. url: https:\/\/arxiv.org\/pdf\/2404.02244.pdf."},{"key":"4_CR13","unstructured":"W. T. Gowers et al. \u201cOn a conjecture of Marton\u201d. arXiv:2311.05762v2 [math.NT]. url: https:\/\/arxiv.org\/pdf\/2311.05762.pdf."},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Jason Gross et al. \u201cAutomatic Test-Case Reduction in Proof Assistants: A Case Study in Coq\u201d. In: 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel. Ed. by June Andronick and Leonardo de Moura. Vol. 237. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022, 18:1\u201318:18. doi: https:\/\/doi.org\/10.4230\/LIPICS.ITP.2022.18. url: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.18","DOI":"10.4230\/LIPICS.ITP.2022.18"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Thomas Hales et al. \u201cA formal proof of the Kepler conjecture\u201d. In: Forum Math. Pi 5 (2017), e2, 29. doi: https:\/\/doi.org\/10.1017\/fmp.2017.1. url: https:\/\/doi.org\/10.1017\/fmp.2017.1.","DOI":"10.1017\/fmp.2017.1"},{"key":"4_CR16","unstructured":"Graydon Hoare. \u201ctechnicalities: \"not rocket science\" (the story of monotone and bors)\u201d. Feb. 2014. url: https:\/\/graydon2.dreamwidth.org\/1597.html."},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Fabian Huch. \u201cIsabelle as Systems Platform: Managing Automated and Quasi-interactive Builds\u201d. In: CoRR abs\/2412.13083 (2024). doi: https:\/\/doi.org\/10.48550\/ARXIV.2412.13083. url: https:\/\/doi.org\/10.48550\/arXiv.2412.13083.","DOI":"10.48550\/ARXIV.2412.13083"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Fabian Huch and Makarius Wenzel. \u201cDistributed Parallel Build for the Isabelle Archive of Formal Proofs\u201d. In: 15th International Conference on Interactive Theorem Proving (ITP 2024). Ed. by Yves Bertot, Temur Kutsia, and Michael Norrish. Vol. 309. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2024, 22:1\u201322:19. doi: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.22. url: https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024. 22.","DOI":"10.4230\/LIPIcs.ITP.2024.22"},{"key":"4_CR19","unstructured":"Jyun-Jie Liao. \u201cImproved Exponent for Marton\u2019s Conjecture in $$F^n_2$$ \u201d. arXiv:2404.09639 [math.CO]. url: https:\/\/arxiv.org\/pdf\/2404.09639.pdf."},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Jannis Limperg and Asta Halkj\u00e6r From. \u201cAesop: White-Box Best-First Proof Search for Lean\u201d. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023. Ed. by Robbert Krebbers et al. ACM, 2023, pp. 253\u2013266. doi: https:\/\/doi.org\/10.1145\/3573105.3575671. url: https:\/\/doi.org\/10.1145\/3573105.3575671.","DOI":"10.1145\/3573105.3575671"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Xiaokun Luan et al. \u201cWhy the Proof Fails in Different Versions of Theorem Provers: An Empirical Study of Compatibility Issues in Isabelle\u201d. In: Proceedings of the ACM on Software Engineering (2025). url: https:\/\/api.semanticscholar.org\/CorpusID:277773988.","DOI":"10.1145\/3715787"},{"key":"4_CR22","unstructured":"Assia Mahboubi and Enrico Tassi. Mathematical Components. 2017."},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Patrick Massot. \u201cTeaching Mathematics Using Lean and Controlled Natural Language\u201d. In: 15th International Conference on Interactive Theorem Proving (ITP 2024). Ed. by Yves Bertot, Temur Kutsia, and Michael Norrish. Vol. 309. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, 2024, 27:1\u201327:19. doi: https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.27. url: https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024.27.","DOI":"10.4230\/LIPIcs.ITP.2024.27"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"William McCune. \u201cExperiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval\u201d. In: J. Autom. Reason. 9.2 (1992), pp. 147\u2013167. doi: https:\/\/doi.org\/10.1007\/BF00245458.","DOI":"10.1007\/BF00245458"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Markus de Medeiros et al. \u201cVerified Foundations for Differential Privacy\u201d. In: Proc. ACM Program. Lang. 9.PLDI (June 2025). doi: https:\/\/doi.org\/10.1145\/3729294. url: https:\/\/doi.org\/10.1145\/3729294.","DOI":"10.1145\/3729294"},{"key":"4_CR26","doi-asserted-by":"publisher","unstructured":"Yecine Megdiche, Fabian Huch, and Lukas Stevens. \u201cA Linter for Isabelle: Implementation and Evaluation\u201d. In: CoRR abs\/2207.10424 (2022). doi: https:\/\/doi.org\/10.48550\/ARXIV.2207.10424. url: https:\/\/doi.org\/10.48550\/arXiv.2207. 10424.","DOI":"10.48550\/ARXIV.2207.10424"},{"key":"4_CR27","unstructured":"Bhavik Mehta. Formalising modern research mathematics in real time. Nov. 2023. url: https:\/\/xenaproject.wordpress.com\/2023\/11\/04\/formalising-modern-research-mathematics-in-real-time\/."},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Leonardo de Moura and Sebastian Ullrich. \u201cThe Lean 4 Theorem Prover and Programming Language\u201d. In: Automated Deduction \u2013 CADE 28. Ed. by Andr\u00e9 Platzer and Geoff Sutcliffe. Cham: Springer International Publishing, 2021, pp. 625\u2013635. url: https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"I. V. Ramakrishnan, R. Sekar, and Andrei Voronkov. \u201cTerm Indexing\u201d. In: Handbook of Automated Reasoning (in 2 volumes). Ed. by John Alan Robinson and Andrei Voronkov. Elsevier and MIT Press, 2001, pp. 1853\u20131964. doi: https:\/\/doi.org\/10.1016\/B978-044450813-3\/50028-X.","DOI":"10.1016\/B978-044450813-3\/50028-X"},{"key":"4_CR30","unstructured":"David Renshaw. Searching for Proof Improvements with tryAtEachStep. Conference talk, Lean together 2025. 2025. url: https:\/\/researchseminars.org\/talk\/LeanTogether2025\/8\/."},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Talia Ringer et al. \u201cQED at Large: A Survey of Engineering of Formally Verified Software\u201d. In: Foundations and Trends\u00ae in Programming Languages 5.2-3 (2019), pp. 102\u2013281. doi: https:\/\/doi.org\/10.1561\/2500000045.","DOI":"10.1561\/2500000045"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Peter Scholze. \u201cLiquid tensor experiment\u201d. In: Exp. Math. 31.2 (2022), pp. 349\u2013354. doi: https:\/\/doi.org\/10.1080\/10586458.2021.1926016. url: https:\/\/www.tandfonline.com\/doi\/full\/10.1080\/10586458.2021.1926016.","DOI":"10.1080\/10586458.2021.1926016"},{"key":"4_CR33","unstructured":"Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. Tabled Typeclass Resolution. 2020. url: https:\/\/arxiv.org\/abs\/2001.04301."},{"key":"4_CR34","doi-asserted-by":"publisher","unstructured":"Chengsong Tan et al. \u201cThe Burden of Proof: Automated Tooling for Rapid Iteration on Large Mechanised Proofs\u201d. In: 2025 IEEE\/ACM 13th International Conference on Formal Methods in Software Engineering (FormaliSE). 2025, pp. 34\u201345. doi: https:\/\/doi.org\/10.1109\/FormaliSE66629.2025.00010.","DOI":"10.1109\/FormaliSE66629.2025.00010"},{"key":"4_CR35","doi-asserted-by":"publisher","unstructured":"The mathlib community. \u201cThe Lean mathematical library\u201d. In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020. 2020, pp. 367\u2013381. doi: https:\/\/doi.org\/10.1145\/3372885.3373824. url: https:\/\/doi.org\/10.1145\/3372885.3373824.","DOI":"10.1145\/3372885.3373824"},{"key":"4_CR36","unstructured":"Floris van Doorn, Gabriel Ebner, and Robert Y. Lewis. \u201cMaintaining a Library of Formal Mathematics\u201d. In: Intelligent Computer Mathematics, CICM 2020. Vol. abs\/2004.03673. 2020. url: https:\/\/arxiv.org\/abs\/2004.03673."},{"key":"4_CR37","unstructured":"MakariusWenzel. Isabelle technology for the Archive of Formal Proofs with application to MMT. 2019. url: https:\/\/arxiv.org\/abs\/1905.07244."},{"key":"4_CR38","unstructured":"Th\u00e9o Zimmermann. \u201cChallenges in the collaborative evolution of a proof language and its ecosystem\u201d. Theses. Universit\u00e9 Paris Cit\u00e9, Dec. 2019. url: https:\/\/inria.hal.science\/tel-02451322."},{"key":"4_CR39","unstructured":"Th\u00e9o Zimmermann et al. \u201cExtending the team with a project-specific bot\u201d. In: CoRR abs\/2112.07365 (2021). url: https:\/\/arxiv.org\/abs\/2112.07365."}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07021-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:40:38Z","timestamp":1759844438000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,8]]},"ISBN":["9783032070203","9783032070210"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,8]]},"assertion":[{"value":"8 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brasilia","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2025\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}