{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:49:56Z","timestamp":1776552596501,"version":"3.51.2"},"publisher-location":"Cham","reference-count":53,"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_2","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"21-41","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Automated Mathematical Discovery and\u00a0Verification: Minimizing Pentagons in\u00a0the\u00a0Plane"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2295-1299","authenticated-orcid":false,"given":"Bernardo","family":"Subercaseaux","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7319-4377","authenticated-orcid":false,"given":"John","family":"Mackey","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1525-1382","authenticated-orcid":false,"given":"Ruben","family":"Martins","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1brego, B.M., Fern\u00e1ndez-Merchant, S., Salazar, G.: The rectilinear crossing number of $$k_n$$: closing in (or are we?). In: Pach, J. (ed.) Thirty Essays on Geometric Graph Theory, pp. 5\u201318. Springer, New York, NY (2013). https:\/\/doi.org\/10.1007\/978-1-4614-0110-0_2","DOI":"10.1007\/978-1-4614-0110-0_2"},{"key":"2_CR2","unstructured":"Aichholzer, O.: [empty][colored] $$k$$-gons - Recent results on some Erd\u0151s-Szekeres type problems. In: Proceedings of the EGC2009, pp. 43\u201352 (2009)"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Aichholzer, O., Aurenhammer, F., Krasser, H.: Enumerating order types for small sets with applications. In: Proceedings of the Seventeenth Annual Symposium on Computational Geometry, pp. 11\u201318. SCG \u201901, Association for Computing Machinery, New York, NY, USA, June 2001. https:\/\/doi.org\/10.1145\/378583.378596","DOI":"10.1145\/378583.378596"},{"issue":"3","key":"2_CR4","doi-asserted-by":"publisher","first-page":"421","DOI":"10.7155\/jgaa.00540","volume":"24","author":"O Aichholzer","year":"2020","unstructured":"Aichholzer, O., Duque, F., Fabila-Monroy, R., Garc\u00eda-Quintero, O.E., Hidalgo-Toscano, C.: An ongoing project to improve the rectilinear and the pseudolinear crossing constants. J. Gr. Algorithms Appl. 24(3), 421\u2013432 (2020). https:\/\/doi.org\/10.7155\/jgaa.00540","journal-title":"J. Gr. Algorithms Appl."},{"key":"2_CR5","unstructured":"Aichholzer, O., Duque, F., Fabila-Monroy, R., Hidalgo-Toscano, C., Garc\u00eda-Quintero, O.E.: An ongoing project to improve the rectilinear and the pseudolinear crossing constants, July 2019. https:\/\/arxiv.org\/abs\/1907.07796v5"},{"issue":"7","key":"2_CR6","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1016\/j.comgeo.2014.12.007","volume":"48","author":"O Aichholzer","year":"2015","unstructured":"Aichholzer, O., et al.: On k-gons and k-holes in point sets. Comput. Geom. 48(7), 528\u2013537 (2015). https:\/\/doi.org\/10.1016\/j.comgeo.2014.12.007","journal-title":"Comput. Geom."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-34191-5_1","volume-title":"Computational Geometry","author":"O Aichholzer","year":"2012","unstructured":"Aichholzer, O., Hackl, T., Vogtenhuber, B.: On 5-Gons and 5-Holes. In: M\u00e1rquez, A., Ramos, P., Urrutia, J. (eds.) EGC 2011. LNCS, vol. 7579, pp. 1\u201313. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34191-5_1"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Appel, K., Haken, W.: The four-color problem. In: Steen, L.A. (ed.) Mathematics Today Twelve Informal Essays, pp. 153\u2013180. Springer, New York, NY (1978). https:\/\/doi.org\/10.1007\/978-1-4613-9435-8_7","DOI":"10.1007\/978-1-4613-9435-8_7"},{"key":"2_CR9","first-page":"12","volume":"2023","author":"F Avellaneda","year":"2023","unstructured":"Avellaneda, F.: Evalmaxsat 2023. MaxSAT Eval. 2023, 12 (2023)","journal-title":"MaxSAT Eval."},{"issue":"2","key":"2_CR10","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1090\/bull\/1832","volume":"61","author":"J Avigad","year":"2024","unstructured":"Avigad, J.: Mathematics and the formal turn. Bull. Am. Math. Soc. 61(2), 225\u2013240 (2024). https:\/\/doi.org\/10.1090\/bull\/1832","journal-title":"Bull. Am. Math. Soc."},{"key":"2_CR11","unstructured":"Bacchus, F., J\u00e4rvisalo, M., Martins, R.: Maximum satisfiabiliy. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 929\u2013991. IOS Press (2021)"},{"key":"2_CR12","doi-asserted-by":"publisher","unstructured":"Berg, J., Bogaerts, B., Nordstr\u00f6m, J., Oertel, A., Vandesande, D.: Certified core-guided MaxSAT solving. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction \u2013 CADE 29. CADE 2023. LNCS, vol. 14132, pp. 1\u201322. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_1","DOI":"10.1007\/978-3-031-38499-8_1"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Bj\u00f6rner, A., Las\u00a0Vergnas, M., Sturmfels, B., White, N., Ziegler, G.M.: Oriented Matroids. Encyclopedia of Mathematics and its Applications, 2 edn. Cambridge University Press, Cambridge (1999). https:\/\/doi.org\/10.1017\/CBO9780511586507","DOI":"10.1017\/CBO9780511586507"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Brakensiek, J., Heule, M., Mackey, J., Narv\u00e1ez, D.: The resolution of keller\u2019s conjecture (2023)","DOI":"10.1007\/s10817-022-09623-5"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Brodsky, A., Durocher, S., Gethner, E.: The rectilinear crossing number of $$k_{10}$$ is $$62$$. Electron. J. Comb. R23 (2001). https:\/\/doi.org\/10.37236\/1567","DOI":"10.37236\/1567"},{"issue":"7993","key":"2_CR16","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1038\/d41586-023-04043-w","volume":"625","author":"D Castelvecchi","year":"2023","unstructured":"Castelvecchi, D.: DeepMind AI outdoes human mathematicians on unsolved problem. Nature 625(7993), 12\u201313 (2023). https:\/\/doi.org\/10.1038\/d41586-023-04043-w","journal-title":"Nature"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-642-40627-0_21","volume-title":"Principles and Practice of Constraint Programming","author":"J Davies","year":"2013","unstructured":"Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247\u2013262. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40627-0_21"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-319-40970-2_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"J Devriendt","year":"2016","unstructured":"Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M.: Improved static symmetry breaking for SAT. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 104\u2013122. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_8"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Eloundou, T., Manning, S., Mishkin, P., Rock, D.: GPTs are GPTs: an early look at the labor market impact potential of large language models (2023)","DOI":"10.1126\/science.adj0998"},{"issue":"1","key":"2_CR20","doi-asserted-by":"publisher","first-page":"52","DOI":"10.2307\/2319261","volume":"80","author":"P Erd\u0151s","year":"1973","unstructured":"Erd\u0151s, P., Guy, R.K.: Crossing number problems. Am. Math. Mon. 80(1), 52\u201358 (1973). https:\/\/doi.org\/10.2307\/2319261","journal-title":"Am. Math. Mon."},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/S0166-218X(00)00232-8","volume":"109","author":"S Felsner","year":"2001","unstructured":"Felsner, S., Weil, H.: Sweeps, arrangements and signotopes. Discret. Appl. Math. 109(1), 67\u201394 (2001). https:\/\/doi.org\/10.1016\/S0166-218X(00)00232-8","journal-title":"Discret. Appl. Math."},{"issue":"4","key":"2_CR22","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0925-7721(00)00010-9","volume":"16","author":"A Garc\u00eda","year":"2000","unstructured":"Garc\u00eda, A., Noy, M., Tejel, J.: Lower bounds on the number of crossing-free subgraphs of $$K_n$$. Comput. Geom. 16(4), 211\u2013221 (2000). https:\/\/doi.org\/10.1016\/S0925-7721(00)00010-9","journal-title":"Comput. Geom."},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Gardi, F., Benoist, T., Darlay, J., Estellon, B., Megel, R.: Mathematical Programming Solver Based on Local Search. Wiley, Hoboken (2014). https:\/\/doi.org\/10.1002\/9781118966464","DOI":"10.1002\/9781118966464"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Goaoc, X., Hubard, A., de\u00a0Joannis\u00a0de Verclos, R., Sereni, J.S., Volec, J.: Limits of order types. In: Arge, L., Pach, J. (eds.) 31st International Symposium on Computational Geometry (SoCG 2015). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a034, pp. 300\u2013314. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2015). https:\/\/doi.org\/10.4230\/LIPIcs.SOCG.2015.300","DOI":"10.4230\/LIPIcs.SOCG.2015.300"},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Gocht, S., Martins, R., Nordstr\u00f6m, J., Oertel, A.: Certified CNF translations for pseudo-Boolean solving. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022. LIPIcs, vol.\u00a0236, pp. 16:1\u201316:25. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.16","DOI":"10.4230\/LIPIcs.SAT.2022.16"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI\u00a0\u201921), pp. 3768\u20133777, February 2021","DOI":"10.1609\/aaai.v35i5.16494"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87827-8_28","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"2_CR28","unstructured":"Gonthier, G.: A computer-checked proof of the Four Color Theorem. Technical report, Inria, March 2023. https:\/\/inria.hal.science\/hal-04034866"},{"issue":"1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1038\/scientificamerican0790-112","volume":"263","author":"RL Graham","year":"1990","unstructured":"Graham, R.L., Spencer, J.H.: Ramsey theory. Sci. Am. 263(1), 112\u2013117 (1990)","journal-title":"Sci. Am."},{"key":"2_CR30","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kullmann, O., Biere, A.: Cube-and-conquer for satisfiability. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 31\u201359. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-63516-3_2","DOI":"10.1007\/978-3-319-63516-3_2"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"2_CR32","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Scheucher, M.: Happy ending: an empty hexagon in every set of 30 points. In: Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, 6\u201311 April 2024, Proceedings, Part I, pp. 61\u201380 (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_5","DOI":"10.1007\/978-3-031-57246-3_5"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1007\/11564751_62","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"A Ishtaiwi","year":"2005","unstructured":"Ishtaiwi, A., Thornton, J., Sattar, A., Pham, D.N.: Neighbourhood clause weight redistribution in local search for SAT. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 772\u2013776. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11564751_62"},{"key":"2_CR34","doi-asserted-by":"publisher","unstructured":"Knuth, D.E.: Axioms and Hulls, pp. 1\u201398. LNCS, Springer, Berlin, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55611-7_1","DOI":"10.1007\/3-540-55611-7_1"},{"key":"2_CR35","doi-asserted-by":"crossref","unstructured":"Konev, B., Lisitsa, A.: A SAT attack on the erdos discrepancy conjecture (2014)","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"2_CR36","unstructured":"Li, C., Xu, Z., Coll, J., Many\u00e0, F., Habet, D., He, K.: Combining clause learning and branch and bound for maxsat. In: Michel, L.D. (ed.) 27th International Conference on Principles and Practice of Constraint Programming. LIPIcs, vol.\u00a0210, pp. 38:1\u201338:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-89960-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Metin","year":"2018","unstructured":"Metin, H., Baarir, S., Colange, M., Kordon, F.: CDCLSym: introducing effective symmetry breaking in SAT solving. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 99\u2013114. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_6"},{"key":"2_CR38","doi-asserted-by":"publisher","unstructured":"Morris, W., Soltan, V.: The Erd\u0151s-Szekeres problem on points in convex position - a survey. Bull. Am. Math. Soc. 37(4), 437\u2013458 (2000). https:\/\/doi.org\/10.1090\/S0273-0979-00-00877-6","DOI":"10.1090\/S0273-0979-00-00877-6"},{"key":"2_CR39","first-page":"20","volume":"2018","author":"T Paxian","year":"2018","unstructured":"Paxian, T., Reimer, S., Becker, B.: Pacose: an iterative sat-based MaxSAT solver. MaxSAT Eval. 2018, 20 (2018)","journal-title":"MaxSAT Eval."},{"issue":"7995","key":"2_CR40","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1038\/s41586-023-06924-6","volume":"625","author":"B Romera-Paredes","year":"2024","unstructured":"Romera-Paredes, B., et al.: Mathematical discoveries from program search with large language models. Nature 625(7995), 468\u2013475 (2024). https:\/\/doi.org\/10.1038\/s41586-023-06924-6","journal-title":"Nature"},{"issue":"10","key":"2_CR41","doi-asserted-by":"publisher","first-page":"939","DOI":"10.2307\/2975158","volume":"101","author":"ER Scheinerman","year":"1994","unstructured":"Scheinerman, E.R., Wilf, H.S.: The rectilinear crossing number of a complete graph and Sylvester\u2019s \u201cfour point problem\u2019\u2019 of geometric probability. Am. Math. Mon. 101(10), 939\u2013943 (1994). https:\/\/doi.org\/10.2307\/2975158","journal-title":"Am. Math. Mon."},{"key":"2_CR42","doi-asserted-by":"publisher","unstructured":"Scheucher, M.: Two disjoint 5-holes in point sets. Comput. Geom. 91 (2020). https:\/\/doi.org\/10.1016\/j.comgeo.2020.101670","DOI":"10.1016\/j.comgeo.2020.101670"},{"key":"2_CR43","doi-asserted-by":"publisher","unstructured":"Scheucher, M.: A sat attack on Erd\u0151s-Szekeres numbers in $$r^d$$ and the empty hexagon theorem. Comput. Geom. Topol. 2(1), 2:1\u20132:13 (2023). https:\/\/doi.org\/10.57717\/cgt.v2i1.12","DOI":"10.57717\/cgt.v2i1.12"},{"key":"2_CR44","doi-asserted-by":"publisher","unstructured":"Shor, P.W.: Stretchability of pseudolines is NP-hard. In: Gritzmann, P., Sturmfels, B. (eds.) Applied Geometry And Discrete Mathematics, Proceedings of a DIMACS Workshop, Providence, Rhode Island, USA, 18 September 1990. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a04, pp. 531\u2013554. DIMACS\/AMS (1990). https:\/\/doi.org\/10.1090\/dimacs\/004\/41","DOI":"10.1090\/dimacs\/004\/41"},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 367\u2013373. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"2_CR46","doi-asserted-by":"publisher","unstructured":"Subercaseaux, B., Heule, M.: Toward optimal radio colorings of hypercubes via sat-solving. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a094, pp. 386\u2013404. EasyChair (2023). https:\/\/doi.org\/10.29007\/qrmp","DOI":"10.29007\/qrmp"},{"key":"2_CR47","doi-asserted-by":"publisher","unstructured":"Subercaseaux, B., Heule, M.J.H.: The packing chromatic number of the infinite square grid is 15. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2023. LNCS, vol. 13993, pp. 389\u2013406. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_20","DOI":"10.1007\/978-3-031-30823-9_20"},{"key":"2_CR48","doi-asserted-by":"publisher","unstructured":"Szekeres, G., Peters, L.: Computer solution to the 17-point Erd\u0151s-Szekeres problem. ANZIAM J. 48(2), 151\u2013164 (2006). https:\/\/doi.org\/10.1017\/S144618110000300X","DOI":"10.1017\/S144618110000300X"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/11527695_24","volume-title":"Theory and Applications of Satisfiability Testing","author":"DAD Tompkins","year":"2005","unstructured":"Tompkins, D.A.D., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306\u2013320. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11527695_24"},{"issue":"7995","key":"2_CR50","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1038\/s41586-023-06747-5","volume":"625","author":"TH Trinh","year":"2024","unstructured":"Trinh, T.H., Wu, Y., Le, Q.V., He, H., Luong, T.: Solving olympiad geometry without human demonstrations. Nature 625(7995), 476\u2013482 (2024). https:\/\/doi.org\/10.1038\/s41586-023-06747-5","journal-title":"Nature"},{"key":"2_CR51","doi-asserted-by":"publisher","unstructured":"Tyrrell, F.: New Lower Bounds for Cap Sets, December 2023. https:\/\/doi.org\/10.19086\/da.91076","DOI":"10.19086\/da.91076"},{"key":"2_CR52","doi-asserted-by":"publisher","unstructured":"Vandesande, D., De Wulf, W., Bogaerts, B.: QMaxSATpb: a certified MaxSAT solver. In: Gottlob, G., Inclezan, D., Maratea, M. (eds.) Logic Programming and Nonmonotonic Reasoning. LPNMR 2022. LNCS, vol. 13416, pp. 429\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-15707-3_33","DOI":"10.1007\/978-3-031-15707-3_33"},{"key":"2_CR53","unstructured":"Yang, K., et al.: LeanDojo: theorem proving with retrieval-augmented language models. In: Neural Information Processing Systems (NeurIPS) (2023)"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:35Z","timestamp":1722715415000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_2","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":"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"}}]}}