{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T04:02:02Z","timestamp":1748491322823,"version":"3.41.0"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031669965"},{"type":"electronic","value":"9783031669972"}],"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_6","type":"book-chapter","created":{"date-parts":[[2024,8,3]],"date-time":"2024-08-03T20:03:12Z","timestamp":1722715392000},"page":"91-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formalizing Finite Ramsey Theory in\u00a0Lean\u00a04"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3704-1060","authenticated-orcid":false,"given":"David E.","family":"Narv\u00e1ez","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2398-8353","authenticated-orcid":false,"given":"Cruise","family":"Song","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-7772-9121","authenticated-orcid":false,"given":"Ningxin","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,29]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1515\/INTEG.2009.007","volume":"9","author":"T Ahmed","year":"2009","unstructured":"Ahmed, T.: Some new van der Waerden numbers and some van der Waerden-type numbers. Integers 9(1), 65\u201376 (2009)","journal-title":"Integers"},{"key":"6_CR2","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/978-3-030-28483-1","volume-title":"Proof Technology in Mathematics Research and Teaching","author":"J Avigad","year":"2019","unstructured":"Avigad, J.: Learning logic and proof with an interactive theorem prover. In: Hanna, G., Reid, D.A., de Villiers, M. (eds.) Proof Technology in Mathematics Research and Teaching, pp. 277\u2013290. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-28483-1"},{"key":"6_CR3","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In Balyo,T., Froleyks, N.,\u00a0Heule, M.,\u00a0Iser, M.,\u00a0J\u00e4rvisalo, M.,\u00a0Suda, M. (eds.) Proceedings of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions, vol.\u00a0B-2020-1 of Department of Computer Science Report Series B, University of Helsinki, pp.\u00a051\u201353 (2020)"},{"issue":"4","key":"6_CR4","doi-asserted-by":"publisher","first-page":"619","DOI":"10.4153\/CMB-1964-059-6","volume":"7","author":"P Erd\u0151s","year":"1964","unstructured":"Erd\u0151s, P.: Some remarks on Ramsay\u2019s theorem. Can. Math. Bull. 7(4), 619\u2013622 (1964)","journal-title":"Can. Math. Bull."},{"issue":"1","key":"6_CR5","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/S0195-6698(80)80020-5","volume":"1","author":"P Erd\u0151s","year":"1980","unstructured":"Erd\u0151s, P.: Some applications of Ramsey\u2019s theorem to additive number theory. Eur. J. Comb. 1(1), 43\u201346 (1980)","journal-title":"Eur. J. Comb."},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF02018669","volume":"2","author":"P Erd\u0151s","year":"1972","unstructured":"Erd\u0151s, P., Szemer\u00e9di, A.: On a Ramsey type theorem. Per. Math. Hung. 2, 295\u2013299 (1972)","journal-title":"Per. Math. Hung."},{"key":"6_CR7","unstructured":"Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory, 2nd ed. Wiley-Interscience (1990)"},{"issue":"1","key":"6_CR8","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":"6_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4153\/CJM-1955-001-4","volume":"7","author":"RE Greenwood","year":"1955","unstructured":"Greenwood, R.E., Gleason, A.M.: Combinatorial relations and chromatic graphs. Can. J. Math. 7, 1\u20137 (1955)","journal-title":"Can. J. Math."},{"key":"6_CR10","unstructured":"Gusakov, A., Mehta, B., Miller, K.A.: Formalizing Hall\u2019s marriage theorem in Lean. Tech. Rep. arXiv:2101.00127 [math.CO], Computing Research Repository. arXiv.org\/corr\/ (2021)"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"R6","DOI":"10.37236\/925","volume":"14","author":"PR Herwig","year":"2007","unstructured":"Herwig, P.R., Heule, M.J., van Lambalgen, M., van Maaren, H.: A new method to construct lower bounds for van der Waerden numbers. Electron. J. Comb. 14, R6 (2007)","journal-title":"Electron. J. Comb."},{"issue":"1","key":"6_CR12","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1080\/10586458.2008.10129025","volume":"17","author":"M Kouril","year":"2008","unstructured":"Kouril, M., Paul, J.L.: The van der Waerden number $$w(2,6)$$ is 1132. Exp. Math. 17(1), 53\u201361 (2008)","journal-title":"Exp. Math."},{"key":"6_CR13","unstructured":"Kreuzer, K., Eberl, M. Van der Waerden\u2019s theorem. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Van_der_Waerden.html, Formal proof development"},{"key":"6_CR14","doi-asserted-by":"publisher","unstructured":"Mehta, B.: Formalising the Kruskal-Katona theorem in lean. In: Buzzard, K., Kutsia, T. (eds.) Intelligent Computer Mathematics, vol. 13467, pp.\u00a075\u201391. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_5","DOI":"10.1007\/978-3-031-16681-5_5"},{"issue":"14\u201315","key":"6_CR15","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1016\/j.ipl.2012.05.004","volume":"112","author":"P Pudl\u00e1k","year":"2012","unstructured":"Pudl\u00e1k, P.: A lower bound on the size of resolution proofs of the Ramsey theorem. Inf. Process. Lett. 112(14\u201315), 610\u2013611 (2012)","journal-title":"Inf. Process. Lett."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Radziszowski, S.P.: Small Ramsey numbers. Electron. J. Comb. Dyn. Surv. 1000, DS1 (1994)","DOI":"10.37236\/21"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc. 1, 264\u2013286 (1930)","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"6_CR18","unstructured":"Schur, I.: \u00dcber die kongruenz $$x^m+y^m\\equiv z^m (~{\\rm mod} \\;p)$$. Jahresbericht Der Deutschen Mathematiker-vereinigung 25, 114\u2013116 (1916)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: Stepping stones in the TPTP world. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) Proceedings of the 12th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence (2024)","DOI":"10.1007\/978-3-031-63498-7_3"},{"issue":"1","key":"6_CR20","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1145\/7531.8928","volume":"34","author":"A Urquhart","year":"1987","unstructured":"Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209\u2013219 (1987)","journal-title":"J. ACM"}],"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_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:05:34Z","timestamp":1748412334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66997-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031669965","9783031669972"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66997-2_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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"}}]}}