{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:48:17Z","timestamp":1776509297916,"version":"3.51.2"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032070203","type":"print"},{"value":"9783032070210","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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_16","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T13:41:32Z","timestamp":1759844492000},"page":"279-299","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Exploring proof autoformalization with Mistral on Herald"],"prefix":"10.1007","author":[{"given":"Lucy","family":"Horowitz","sequence":"first","affiliation":[]},{"given":"Michail","family":"Karatarakis","sequence":"additional","affiliation":[]},{"given":"Xuandi","family":"Ren","sequence":"additional","affiliation":[]},{"given":"Alejandro","family":"Sanchez Ocegueda","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Agrawal, A., Gadgil, S., Goyal, N., Narayanan, A., Tadipatri, A.: Towards a Mathematics Formalisation Assistant using Large Language Models (2022), https:\/\/arxiv.org\/abs\/2211.07524"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Azerbayev, Z., Piotrowski, B., Schoelkopf, H., Ayers, E.W., Radev, D., Avigad, J.: ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics (Feb 2023). https:\/\/doi.org\/10.48550\/arXiv.2302.12433","DOI":"10.48550\/arXiv.2302.12433"},{"key":"16_CR3","unstructured":"Azerbayev, Z., Schoelkopf, H., Paster, K., Santos, M.D., McAleer, S., Jiang, A.Q., Deng, J., Biderman, S., Welleck, S.: Llemma: An Open Language Model for Mathematics. In: The Twelfth International Conference on Learning Representations (2024)"},{"key":"16_CR4","unstructured":"Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C., Wilcox, S.: HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA. Proceedings of Machine Learning Research, vol.\u00a097, pp. 454\u2013463. PMLR (2019), http:\/\/proceedings.mlr.press\/v97\/bansal19a.html"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 415\u2013442. Springer International Publishing, Cham (2022)","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Gurfinkel, A., Ganesh, V. (eds.) Computer Aided Verification - 36th International Conference, CAV 2024, Montreal, QC, Canada, July 24-27, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14681, pp. 133\u2013152. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"16_CR7","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL, Gimsatul, IsaSAT and Kissat Entering the SAT Competition 2024. In: Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2024 \u2013 Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Report Series B, vol. B-2024-1, pp. 8\u201310. University of Helsinki (2024)"},{"key":"16_CR8","doi-asserted-by":"publisher","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.) 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0309, pp. 10:1\u201310:20. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.10, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.ITP.2024.10","DOI":"10.4230\/LIPIcs.ITP.2024.10"},{"key":"16_CR9","unstructured":"Gao, G., Wang, Y., Jiang, J., Gao, Q., Qin, Z., Xu, T., Dong, B.: Herald: A Natural Language Annotated Lean 4 Dataset (2025), https:\/\/arxiv.org\/abs\/2410.10878"},{"key":"16_CR10","unstructured":"Han, J.M., Rute, J., Wu, Y., Ayers, E., Polu, S.: Proof Artifact Co-Training for Theorem Proving with Language Models. In: International Conference on Learning Representations (2022), https:\/\/openreview.net\/forum?id=rpxJc9j04U"},{"key":"16_CR11","unstructured":"Huang, D., Dhariwal, P., Song, D., Sutskever, I.: GamePad: A Learning Environment for Theorem Proving. In: International Conference on Learning Representations (ICLR) (2019)"},{"key":"16_CR12","unstructured":"Hughes, C.: Project Euler. https:\/\/projecteuler.net\/ (2001), accessed: 2025-05-24"},{"key":"16_CR13","unstructured":"Jiang, A.Q., Li, W., Jamnik, M.: Multilingual Mathematical Autoformalization. arXiv preprint arXiv:2311.03755 (2023)"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Jiang, A.Q., Welleck, S., Zhou, J.P., Li, W., Liu, J., Jamnik, M., Lacroix, T., Wu, Y., Lample, G.: Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (Feb 2023). https:\/\/doi.org\/10.48550\/arXiv.2210.12283","DOI":"10.48550\/arXiv.2210.12283"},{"key":"16_CR15","unstructured":"Jiang, A.Q., Li, W., Han, J.M., Wu, Y.: LISA: Language Models of ISAbelle Proofs. In: Conference on Artificial Intelligence and Theorem Proving (AITP) (2021)"},{"key":"16_CR16","unstructured":"Jiang, A.Q., Li, W., Tworkowski, S., Czechowski, K., Odrzyg\u00f3\u017ad\u017a, T., Mi\u0142o\u015b, P., Wu, Y., Jamnik, M.: Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In: Proceedings of the 36th International Conference on Neural Information Processing Systems (2022)"},{"key":"16_CR17","unstructured":"Kaliszyk, C., Chollet, F., Szegedy, C.: HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In: International Conference on Learning Representations (ICLR) (2017)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Automating Formalization by Statistical and Semantic Parsing of Mathematics. In: ITP. LNCS, vol. 10499, pp. 12\u201327 (2017)","DOI":"10.1007\/978-3-319-66107-0_2"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J., Geuvers, H.: Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description. In: CICM 2014. LNCS, vol.\u00a08543, pp. 435\u2013439 (2014)","DOI":"10.1007\/978-3-319-08434-3_34"},{"key":"16_CR20","unstructured":"Karatarakis, M.: Leveraging Large Language odels for Autoformalizing Theorems: A Case Study. In: Artificial Intelligence and Theorem Proving (AITP). Aussois, France (2024)"},{"key":"16_CR21","unstructured":"Lample, G., Lachaux, M.A., Lavril, T., Martinet, X., Hayat, A., Ebner, G., Rodriguez, A., Lacroix, T.: HyperTree Proof Search for Neural Theorem Proving (2022), https:\/\/arxiv.org\/abs\/2205.11491"},{"key":"16_CR22","unstructured":"Li, W., Yu, L., Wu, Y., Paulson, L.C.: IsarStep: a Benchmark for High-level Mathematical Reasoning. In: International Conference on Learning Representations (ICLR) (2021)"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Limperg, J., From, A.H.: Aesop: White-Box Best-First Proof Search for Lean. In: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs. p. 253\u2013266. CPP 2023, Association for Computing Machinery, New York, NY, USA (2023). https:\/\/doi.org\/10.1145\/3573105.3575671, https:\/\/doi.org\/10.1145\/3573105.3575671","DOI":"10.1145\/3573105.3575671"},{"key":"16_CR24","unstructured":"Lin, H., Sun, Z., Yang, Y., Welleck, S.: Lean-STaR: Learning to Interleave Thinking and Proving (2024), https:\/\/arxiv.org\/abs\/2407.10040"},{"key":"16_CR25","unstructured":"Miku\u0142a, M., Antoniak, S., Tworkowski, S., Jiang, A.Q., Zhou, J.P., Szegedy, C., Kuci\u0144ski, \u0141., Mi\u0142o\u015b, P., Wu, Y.: Magnushammer: A Transformer-Based Approach to Premise Selection. arXiv preprint arXiv:2303.04488 (2023)"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Mohamed, A., Mascarenhas, T., Khan, H., Barbosa, H., Reynolds, A., Qian, Y., Tinelli, C., Barrett, C.: Lean-SMT: An SMT Tactic for Discharging Proof Goals in Lean (2025), https:\/\/arxiv.org\/abs\/2505.15796","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean Theorem Prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25. pp. 378\u2013388. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"16_CR28","unstructured":"Patel, N., Flanigan, J., Saha, R.: A New Approach Towards Autoformalization. arXiv preprint arXiv:2310.07957 (2023)"},{"key":"16_CR29","unstructured":"Polu, S., Han, J.M., Zheng, K., Baksys, M., Babuschkin, I., Sutskever, I.: Formal Mathematics Statement Curriculum Learning (2022), https:\/\/arxiv.org\/abs\/2202.01344"},{"key":"16_CR30","unstructured":"Reichel, T., Henderson, R., Touchet, A., Gardner, A., Ringer, T.: Proof Repair Infrastructure for Supervised Models: Building a Large Proof Repair Dataset. In: International Conference on Interactive Theorem Proving (ITP) (2023)"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Ren, Z.Z., Shao, Z., Song, J., Xin, H., Wang, H., Zhao, W., Zhang, L., Fu, Z., Zhu, Q., Yang, D., Wu, Z.F., Gou, Z., Ma, S., Tang, H., Liu, Y., Gao, W., Guo, D., Ruan, C.: DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition (Apr 2025). https:\/\/doi.org\/10.48550\/arXiv.2504.21801","DOI":"10.48550\/arXiv.2504.21801"},{"key":"16_CR32","unstructured":"Shao, Z., Wang, P., Zhu, Q., Xu, R., Song, J., Zhang, M., Li, Y., Wu, Y., Guo, D.: DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models. arXiv preprint arXiv:2402.03300 (2024)"},{"key":"16_CR33","unstructured":"The Lean Prover Community: BVDecide (2025), https:\/\/leanprover-community.github.io\/mathlib4_docs\/Lean\/Elab\/Tactic\/BVDecide.html"},{"key":"16_CR34","unstructured":"The Lean Prover Community: Grind (2025), https:\/\/leanprover-community.github.io\/mathlib4_docs\/Init\/Grind\/Tactics.html"},{"key":"16_CR35","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. p. 367\u2013381. CPP 2020, Association for Computing Machinery, New York, NY, USA (2020). https:\/\/doi.org\/10.1145\/3372885.3373824, https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"},{"key":"16_CR36","unstructured":"Wang, H., Xin, H., Zheng, C., Li, L., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., Yin, J., Li, Z., Liao, H., Liang, X.: LEGO-Prover: Neural Theorem Proving with Growing Libraries (2023)"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Wang, Q., Kaliszyk, C., Urban, J.: First Experiments with Neural Translation of Informal to Formal Mathematics. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings. Lecture Notes in Computer Science, vol. 11006, pp. 255\u2013270. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22, https:\/\/doi.org\/10.1007\/978-3-319-96812-4_22","DOI":"10.1007\/978-3-319-96812-4_22"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Wang, R., Zhang, J., Jia, Y., Pan, R., Diao, S., Pi, R., Zhang, T.: TheoremLlama: ransforming General-Purpose LLMs into Lean4 Experts. arXiv preprint arXiv:2407.03203 (2024)","DOI":"10.18653\/v1\/2024.emnlp-main.667"},{"key":"16_CR39","unstructured":"Welleck, S., Saha, R.: LLMSTEP: LLM Proofstep Suggestions in Lean. arXiv preprint arXiv:2310.18457 (2023)"},{"key":"16_CR40","unstructured":"Wu, Y., Jiang, A.Q., Li, W., Rabe, M., Staats, C., Jamnik, M., Szegedy, C.: Autoformalization with Large Language Models. In: Proceedings of the 36th International Conference on Neural Information Processing Systems (2022)"},{"key":"16_CR41","unstructured":"Xin, H., Guo, D., Shao, Z., Ren, Z., Zhu, Q., Liu, B., Ruan, C., Li, W., Liang, X.: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data. arXiv preprint arXiv:2405.14333 (2024)"},{"key":"16_CR42","unstructured":"Xin, H., Wang, H., Zheng, C., Li, L., Liu, Z., Cao, Q., Huang, Y., Xiong, J., Shi, H., Xie, E., et\u00a0al.: LEGO-Prover: Neural Theorem Proving with Growing Libraries. In: The Twelfth International Conference on Learning Representations (2024)"},{"key":"16_CR43","unstructured":"Yang, K., Deng, J.: Learning to Prove Theorems via Interacting with Proof Assistants. In: International Conference on Machine Learning (ICML) (2019)"},{"key":"16_CR44","unstructured":"Yang, K., Swope, A., Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., Anandkumar, A.: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In: Proceedings of the 37th International Conference on Neural Information Processing Systems (2023)"},{"key":"16_CR45","unstructured":"Ying, H., Wu, Z., Geng, Y., Wang, J., Lin, D., Chen, K.: Lean Workbook: A Large-Scale Lean Problem Set Formalized from Natural Language Math Problems (2024), https:\/\/arxiv.org\/abs\/2406.03847"},{"key":"16_CR46","unstructured":"Ying, H., Zhang, S., Li, L., Zhou, Z., Shao, Y., Fei, Z., Ma, Y., Hong, J., Liu, K., Wang, Z., Wang, Y., Wu, Z., Li, S., Zhou, F., Liu, H., Zhang, S., Zhang, W., Yan, H., Qiu, X., Wang, J., Chen, K., Lin, D.: InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning (2024), https:\/\/arxiv.org\/abs\/2402.06332"},{"key":"16_CR47","doi-asserted-by":"publisher","unstructured":"Zheng, K., Han, J.M., Polu, S.: MiniF2F: a Cross-system Benchmark for Formal Olympiad-level Mathematics (2022). https:\/\/doi.org\/10.48550\/arXiv.2109.00110","DOI":"10.48550\/arXiv.2109.00110"},{"key":"16_CR48","unstructured":"Zhou, J.P., Staats, C.E., Li, W., Szegedy, C., Weinberger, K.Q., Wu, Y.: Don\u2019t Trust: Verify\u2013Grounding LLM Quantitative Reasoning with Autoformalization. In: The Twelfth International Conference on Learning Representations (2024)"},{"key":"16_CR49","unstructured":"Zhu, T., Clune, J., Avigad, J., Jiang, A.Q., Welleck, S.: Premise Selection for a Lean Hammer (2025), https:\/\/arxiv.org\/abs\/2506.07477"}],"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_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T10:21:43Z","timestamp":1776507703000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07021-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032070203","9783032070210"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07021-0_16","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":"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"}}]}}