{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:55Z","timestamp":1784804455855,"version":"3.55.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>In the context of the Equational Theories Project, Terence Tao posed the challenge of finding alternatives to a complicated 62-step proof found by the Vampire superposition prover. We introduce a proof minimization tool called Krympa. Using a combination of brute force and heuristics, and exploiting both Vampire and the Twee equational prover, the tool reduces the 62-step proof to 20\u00a0steps, each corresponding to a rewrite. In an empirical evaluation, it also performs well on 1431 equational problems originating from the same project, reducing in particular a 151-step proof to only 10\u00a0steps.<\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_1","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:03:32Z","timestamp":1784801012000},"page":"3-21","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Tao\u2019s Equational Proof Challenge Accepted"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-9875-2627","authenticated-orcid":false,"given":"Lydia","family":"Kondylidou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8367-0936","authenticated-orcid":false,"given":"Jasmin","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5587-8801","authenticated-orcid":false,"given":"Marijn J. H.","family":"Heule","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Amjad, H.: Compressing propositional refutations. In: Merz, S., Nipkow, T. (eds.) AVoCS 2006. Electronic Notes in Theoretical Computer Science, vol.\u00a0185, pp. 3\u201315. Elsevier (2006)","DOI":"10.1016\/j.entcs.2007.05.025"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Dershowitz, N., Plaisted, D.A.: Completion without failure. In: A\u00eft-Kaci, H., Nivat, M. (eds.) Rewriting Techniques, pp. 1\u201330. Academic Press (1989)","DOI":"10.1016\/B978-0-12-046371-8.50007-9"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Strict basic superposition. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 160\u2013174. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054258","DOI":"10.1007\/BFb0054258"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"B\u00e1rtek, F., et al.: The Vampire diary. In: Piskac, R., Rakamaric, Z. (eds.) CAV 2025. LNCS, vol. 15933, pp. 57\u201371. Springer (2025)","DOI":"10.1007\/978-3-031-98682-6_4"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Automated Reas. 56, 155\u2013200 (2016)","journal-title":"J. Automated Reas."},{"key":"1_CR6","unstructured":"Bolan, M.: The Equational Theories Project (2025)"},{"key":"1_CR7","unstructured":"Buch, A., Hillenbrand, T.: WALDMEISTER: development of a high performance completion-based theorem prover. Tech. rep. (1996)"},{"key":"1_CR8","unstructured":"Clune, J., Qian, Y., Bentkamp, A., Avigad, J.: Duper: a proof-producing superposition theorem prover for dependent type theory. In: Bertot, Y., Kutsia, T., Norrish, M. (eds.) ITP 2024. LIPIcs, vol.\u00a0309, pp. 1\u201320. Leibniz-Zentrum f\u00fcr Informatik (2024)"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Cotton, S.: Two techniques for minimizing resolution proofs. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 306\u2013312. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14186-7_26","DOI":"10.1007\/978-3-642-14186-7_26"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Denzinger, J., Schulz, S.: Recording, analyzing and presenting distributed deduction processes. In: Hong, H. (ed.) PASCO 1994. Lecture Notes Series in Computing, vol.\u00a05, pp. 114\u2013123. World Scientific (1994)","DOI":"10.1142\/9789814533584_0012"},{"key":"1_CR11","unstructured":"Floch, B.L.: Zulip post in \u201cMachine Learning for Theorem Proving: A (Semi)-Autoformalization Challenge (650 $$\\rightarrow $$ 448)\u201d. Zulip (2025). https:\/\/leanprover.zulipchat.com\/#narrow\/channel\/219941-Machine-Learning-for-Theorem-Proving\/topic\/A.20.28semi.29-autoformalization.20challenge.3A.20650.3D.3E448\/near\/518970125"},{"key":"1_CR12","unstructured":"Floch, B.L.: Zulip post in \u201cMachine Learning for Theorem Proving: A (Semi)-Autoformalization Challenge (650 $$\\rightarrow $$ 448)\u201d. Zulip (2025). https:\/\/leanprover.zulipchat.com\/#narrow\/channel\/219941-Machine-Learning-for-Theorem-Proving\/topic\/A.20.28semi.29-autoformalization.20challenge.3A.20650.3D.3E448\/near\/568313777"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: Stepping stones in the TPTP World. In: Benzm\u00fcller, C., Heule, M., Schmidt, R. (eds.) IJCAR 2024. LNCS, pp. 30\u201350 (2024)","DOI":"10.1007\/978-3-031-63498-7_3"},{"key":"1_CR14","unstructured":"Gu, A., Piotrowski, B., Gloeckle, F., Yang, K., Markosyan, A.H.: ProofOptimizer: training language models to simplify proofs without human demonstrations (2025). https:\/\/arxiv.org\/abs\/2510.15700"},{"key":"1_CR15","unstructured":"Hajdu, M., Coutelier, R., Kov\u00e1cs, L., Voronkov, A.: Term ordering diagrams. In: Barrett, C.W., Waldmann, U. (eds.) CADE-30. LNCS. Springer to appear"},{"key":"1_CR16","unstructured":"Janota, M.: Experimental results for vampire on the equational theories project (2025). https:\/\/arxiv.org\/abs\/2508.15856"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing Rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_28"},{"key":"1_CR18","unstructured":"Kinyon, M.: Zulip post in \u201cMachine Learning for Theorem Proving: A (Semi)-Autoformalization Challenge (650 $$\\rightarrow $$ 448)\u201d. Zulip (2025). https:\/\/leanprover.zulipchat.com\/#narrow\/channel\/219941-Machine-Learning-for-Theorem-Proving\/topic\/A.20.28semi.29-autoformalization.20challenge.3A.20650.3D.3E448\/near\/518961204"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Kondylidou, L., Blanchette, J., Heule, M.: Tao\u2019s equational proof challenge accepted. Zenodo (2026). https:\/\/doi.org\/10.5281\/zenodo.18624123","DOI":"10.5281\/zenodo.18624123"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Limperg, J., From, A.H.: Aesop: white-box best-first proof search for Lean. In: CPP 2023, pp. 253\u2013266. ACM (2023)","DOI":"10.1145\/3573105.3575671"},{"key":"1_CR22","unstructured":"McCune, W.: Prover9 and Mace4 (2005\u20132010)"},{"key":"1_CR23","unstructured":"Morrison, K., de\u00a0Moura, L.: grind: an SMT-inspired tactic for Lean 4 (short paper\u2014system description). In: Biere, A., Lutz, C., Negri, S. (eds.) IJCAR 2026. LNCS, Springer"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated deduction \u2013 CADE 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.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"1_CR25","unstructured":"Norman, C., Avigad, J.: Canonical for automated theorem proving in lean. In: ITP 2025. LIPIcs, vol.\u00a0352, pp. 1\u201320. Leibniz-Zentrum f\u00fcr Informatik (2025)"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-030-79876-5_35","volume-title":"Automated Deduction \u2013 CADE 28","author":"N Smallbone","year":"2021","unstructured":"Smallbone, N.: Twee: an equational theorem prover. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 602\u2013613. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_35"},{"issue":"1","key":"1_CR27","first-page":"129","volume":"14","author":"Z Stachniak","year":"1991","unstructured":"Stachniak, Z.: Minimization of resolution proof systems. Fundam. Inf. 14(1), 129\u2013146 (1991)","journal-title":"Fundam. Inf."},{"key":"1_CR28","first-page":"3","volume":"38","author":"G Sutcliffe","year":"2025","unstructured":"Sutcliffe, G.: The 12th IJCAR automated theorem proving system competition\u2013CASC-J12. AI Commun. 38, 3\u201320 (2025)","journal-title":"AI Commun."},{"key":"1_CR29","unstructured":"Sutcliffe, G., Chang, C., McGuinness, D., Lebo, T., Ding, L., da\u00a0Silva, P.P.: Combining proofs to form different proofs. In: Fontaine, P., Stump, A. (eds.) PxTP 2011, pp. 60\u201373. LNCS (2011)"},{"key":"1_CR30","unstructured":"Tao, T.: Zulip thread \u201cMachine Learning for Theorem Proving: A (Semi)-Autoformalization Challenge (650 $$\\rightarrow $$ 448)\u201d. Zulip (2025). https:\/\/leanprover-community.github.io\/archive\/stream\/219941-Machine-Learning-for-Theorem-Proving\/"},{"key":"1_CR31","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/978-3-642-17511-4_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J Vysko\u010dil","year":"2010","unstructured":"Vysko\u010dil, J., Stanovsk\u00fd, D., Urban, J.: Automated proof compression by invention of new definitions. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 447\u2013462. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_25"},{"key":"1_CR32","unstructured":"Zhu, T., Clune, J., Avigad, J., Jiang, A.Q., Welleck, S.: Premise selection for a Lean hammer (2026). https:\/\/arxiv.org\/abs\/2506.07477"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:03:44Z","timestamp":1784801024000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","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 paper.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}