{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T05:55:17Z","timestamp":1769579717722,"version":"3.49.0"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031669965","type":"print"},{"value":"9783031669972","type":"electronic"}],"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-66997-2_9","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"146-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Incorporating a\u00a0Database of\u00a0Graphs into\u00a0a\u00a0Proof Assistant"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5378-0547","authenticated-orcid":false,"given":"Andrej","family":"Bauer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6678-8975","authenticated-orcid":false,"given":"Katja","family":"Ber\u010di\u010d","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3931-1610","authenticated-orcid":false,"given":"Gauvain","family":"Devillez","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6593-6796","authenticated-orcid":false,"given":"Jure","family":"Taslak","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Abdulaziz, M., Mehlhorn, K., Nipkow, T.: Trustworthy graph algorithms. In: Rossmanith, P., Heggernes, P., Katoen, J.P. (eds.) 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0138, pp. 1:1\u20131:22. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2019). https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.1","DOI":"10.4230\/LIPIcs.MFCS.2019.1"},{"key":"9_CR2","unstructured":"Bauer, A., Ber\u010di\u010d, K., Devillez, G., Taslak, J.: Lean-HoG (2024). https:\/\/github.com\/katjabercic\/Lean-HoG\/"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Blum, M., Kanna, S.: Designing programs that check their work. In: STOC\u201989: Proceedings of the Twenty-First Annual ACM Symposium on Theory of Computing, pp. 86\u201397, February 1989. https:\/\/doi.org\/10.1145\/200836.200880","DOI":"10.1145\/200836.200880"},{"key":"9_CR4","unstructured":"Carneiro, M.: The Type Theory of Lean. Master\u2019s thesis, Carnegie Mellon University, Pittsburgh (2019)"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Codel, C.R., Avigad, J., Heule, M.J.H.: Verified encodings for SAT solvers. in: Nadel, A., Rozier, K.Y. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2023, Ames, IA, USA, 24\u201327 October 2023, pp. 141\u2013151. IEEE (2023). https:\/\/doi.org\/10.34727\/2023\/isbn.978-3-85448-060-0_22","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_22"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Coolsaet, K., D\u2019Hondt, S., Goedgebeur, J.: House of Graphs 2.0: a database of interesting graphs and more. Discrete Appl. Math. 325, 97\u2013107 (2023)","DOI":"10.1016\/j.dam.2022.10.013"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-14808-8_18","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"A Darbari","year":"2010","unstructured":"Darbari, A., Fischer, B., Marques-Silva, J.: Industrial-strength certified sat solving through verified sat proof checking. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 260\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14808-8_18"},{"key":"9_CR8","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":"9_CR9","doi-asserted-by":"publisher","unstructured":"Diestel, R.: Graph Theory: 5th edition. Springer Graduate Texts in Mathematics, Springer-Verlag (2017). https:\/\/doi.org\/10.1007\/978-3-662-53622-3","DOI":"10.1007\/978-3-662-53622-3"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Franz, M., Lopes, C.T., Huck, G., Dong, Y., Sumer, O., Bader, G.D.: Cytoscape.js: a graph theory library for visualisation and analysis. Bioinformatics 32(2), 309\u2013311 (2015). https:\/\/doi.org\/10.1093\/bioinformatics\/btv557","DOI":"10.1093\/bioinformatics\/btv557"},{"key":"9_CR11","unstructured":"Gocht, S.: Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning. Ph.D. thesis, Lund University, Lund, Sweden, June 2022. https:\/\/lucris.lub.lu.se\/ws\/portalfiles\/portal\/117886509\/thesis_final_pdf.pdf"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Gocht, S., McBride, R., McCreesh, C., Nordstr\u00f6m, J., Prosser, P., Trimble, J.: Certifying solvers for clique and maximum common (connected) subgraph problems. In: The 26th International Conference on Principles and Practice of Constraint Programming, pp. 338\u2013357, September 2020. https:\/\/doi.org\/10.1007\/978-3-030-58475-7_20","DOI":"10.1007\/978-3-030-58475-7_20"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Subgraph isomorphism meets cutting planes: Solving with certified solutions. In: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, pp. 1134\u20131140, January 2021. https:\/\/doi.org\/10.24963\/ijcai.2020\/158","DOI":"10.24963\/ijcai.2020\/158"},{"key":"9_CR14","unstructured":"Gowers, W.T., Green, B., Manners, F., Tao, T.: On a conjecture of Marton. arXiv:2311.05762, December 2023"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Le\u00a0Truong, H., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., et\u00a0al.: A formal proof of the kepler conjecture. In: Forum of mathematics, Pi. vol.\u00a05, p.\u00a0e2. Cambridge University Press (2017). https:\/\/doi.org\/10.1017\/fmp.2017.1","DOI":"10.1017\/fmp.2017.1"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Harrison, J., Th\u00e9ry, L.: A skeptic\u2019s approach to combining HOL and Maple. Journal of Automated Reasoning 21(3) (1998). https:\/\/doi.org\/10.1023\/A:1006023127567","DOI":"10.1023\/A:1006023127567"},{"key":"9_CR17","unstructured":"House of Graphs. https:\/\/houseofgraphs.org"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Karp, R.M.: 50 Years of Integer Programming 1958-2008: From the Early Years to the State-of-the-Art, chap. Reducibility Among Combinatorial Problems, pp. 219\u2013241. Springer Berlin Heidelberg, Berling, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-540-68279-0","DOI":"10.1007\/978-3-540-68279-0"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Lammich, P.: The GRAT tool chain: Efficient (UN)SAT certificate checking with formal correctness guarantees. In: Theory and Applications of Satisfiability Testing\u2013SAT 2017: 20th International Conference, Melbourne, VIC, Australia, August 28\u2013September 1, 2017, Proceedings 20. pp. 457\u2013463. Springer (2017). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","DOI":"10.1007\/s10817-019-09525-z"},{"key":"9_CR20","unstructured":"Lean forward: Usable computer-checked proofs and computations for number theorists. https:\/\/lean-forward.github.io\/"},{"key":"9_CR21","unstructured":"LeanSAT. https:\/\/github.com\/JamesGallicchio\/LeanSAT"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Lewis, R.Y., Wu, M.: A bi-directional extensible interface between Lean and Mathematica. Journal of Automated Reasoning 66(2) (2022)","DOI":"10.1007\/s10817-021-09611-1"},{"key":"9_CR23","unstructured":"LMFDB Collaboration, T.: The L-functions and modular forms database. https:\/\/www.lmfdb.org (2024), [Online; accessed 12 June 2024]"},{"key":"9_CR24","unstructured":"Mathlib community: Completion of the Liquid Tensor Experiment. Lean community blog, July 2022. https:\/\/leanprover-community.github.io\/blog\/posts\/lte-final\/"},{"issue":"2","key":"9_CR25","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"R McConnell","year":"2011","unstructured":"McConnell, R., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.09.009","journal-title":"Computer Science Review"},{"key":"9_CR26","doi-asserted-by":"publisher","DOI":"10.1145\/204865.204889","author":"K Mehlhor","year":"2009","unstructured":"Mehlhor, K., N\u00e4her, S.: LEDA: A Platform for Combinatorial and Geometric Computing. Cambridge University Press (2009). https:\/\/doi.org\/10.1145\/204865.204889","journal-title":"Cambridge University Press"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Nawrocki, W., Ayers, E.W., Ebner, G.: An extensible user interface for Lean 4. In: 14th International Conference on Interactive Theorem Proving (ITP 2023). Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.24","DOI":"10.4230\/LIPIcs.ITP.2023.24"},{"key":"9_CR28","unstructured":"Python Software Foundation: Python language reference. https:\/\/www.python.org"},{"key":"9_CR29","unstructured":"Expression quotations for Lean 4. https:\/\/github.com\/leanprover-community\/quote4"},{"key":"9_CR30","unstructured":"SageMath. https:\/\/www.sagemath.org"},{"key":"9_CR31","unstructured":"Subercaseaux, B., Nawrocki, W., Gallicchio, J., Codel, C., Carneiro, M., Heule, M.J.H.: Formal Verification of the Empty Hexagon Number. arXiv:2403.17370 (March 2024)"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Tan, Y.K., Heule, M.J., Myreen, M.O.: cake_lpr: Verified propagation redundancy checking in CakeML. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 223\u2013241 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_12","DOI":"10.1007\/978-3-030-72013-1_12"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"The Mathlib Community: 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 (2020). https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"issue":"2","key":"9_CR34","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.entcs.2005.12.007","volume":"144","author":"T Weber","year":"2006","unstructured":"Weber, T.: Integrating a sat solver with an lcf-style theorem prover. Electronic Notes in Theoretical Computer Science 144(2), 67\u201378 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.12.007","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9_CR35","unstructured":"Wolfram Research Inc.: Mathematica. https:\/\/www.wolfram.com\/mathematica"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Zhou, N.F.: In Pursuit of an Efficient SAT Encoding for the Hamiltonian Cycle Problem. In: Simonis, H. (ed.) Principles and Practice of Constraint Programming. pp. 585\u2013602. Springer International Publishing (2020). https:\/\/doi.org\/10.1007\/978-3-030-58475-7_34","DOI":"10.1007\/978-3-030-58475-7_34"}],"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-031-66997-2_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:33Z","timestamp":1748412333000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have 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":"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":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","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":"5 August 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2024\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}