{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T05:49:11Z","timestamp":1769752151271,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T00:00:00Z","timestamp":1720569600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["BD\\\/04736\\\/2023,UIDB\\\/50021\\\/2020"],"award-info":[{"award-number":["BD\\\/04736\\\/2023,UIDB\\\/50021\\\/2020"]}]},{"name":"National Science Foundation","award":["CCF-1955457,CCF-2220892"],"award-info":[{"award-number":["CCF-1955457,CCF-2220892"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,7,10]]},"DOI":"10.1145\/3663529.3663814","type":"proceedings-article","created":{"date-parts":[[2024,7,10]],"date-time":"2024-07-10T19:43:13Z","timestamp":1720640593000},"page":"637-641","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["CoqPyt: Proof Navigation in Python in the Era of LLMs"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4316-928X","authenticated-orcid":false,"given":"Pedro","family":"Carrott","sequence":"first","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4148-5991","authenticated-orcid":false,"given":"Nuno","family":"Saavedra","sequence":"additional","affiliation":[{"name":"INESC-ID, Lisbon, Portugal \/ Instituto Superior T\u00e9cnico, University of Lisbon, Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2868-7612","authenticated-orcid":false,"given":"Kyle","family":"Thompson","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3957-0628","authenticated-orcid":false,"given":"Sorin","family":"Lerner","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6612-9013","authenticated-orcid":false,"given":"Jo\u00e3o F.","family":"Ferreira","sequence":"additional","affiliation":[{"name":"INESC-ID, Lisbon, Portugal \/ Instituto Superior T\u00e9cnico, University of Lisbon, Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2896-2928","authenticated-orcid":false,"given":"Emily","family":"First","sequence":"additional","affiliation":[{"name":"University of California at San Diego, San Diego, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,7,10]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck.","author":"Azerbayev Zhangir","year":"2023","unstructured":"Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2023. Llemma: An Open Language Model For Mathematics. arxiv:2310.10631."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_17"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2204.02311"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510138"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428299"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_2_1_7_1","unstructured":"Emilio Jes\u00fas Gallego Arias. 2016. SerAPI: Machine-Friendly Data-Centric Serialization for Coq. MINES ParisTech. https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01384408"},{"key":"e_1_3_2_1_8_1","unstructured":"Daniel Huang Prafulla Dhariwal Dawn Song and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In ICLR. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7"},{"key":"e_1_3_2_1_9_1","unstructured":"IBM. 2021. pycoq. https:\/\/github.com\/IBM\/pycoq"},{"key":"e_1_3_2_1_10_1","volume-title":"6th Conference on Artificial Intelligence and Theorem Proving, Sept..","author":"Jiang Albert Q.","year":"2021","unstructured":"Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. LISA: Language models of ISAbelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, Sept.."},{"key":"e_1_3_2_1_11_1","volume-title":"Yuhuai Wu, and Mateja Jamnik.","author":"Jiang Albert Qiaochu","year":"2022","unstructured":"Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg\u00f3\u017ad\u017a, Piotr Mi\u0142 o\u015b, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems (NeurIPS 2022, Vol. 35). Curran Associates, Inc., 8360\u20138373."},{"key":"e_1_3_2_1_12_1","volume-title":"The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SMa9EAovKMC","author":"Jiang Albert Qiaochu","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. 2023. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In The Eleventh International Conference on Learning Representations. https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"e_1_3_2_1_13_1","volume-title":"CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert - A Formally Verified Optimizing Compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress. Toulouse, France. https:\/\/inria.hal.science\/hal-01238879"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2206.14858"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_44"},{"key":"e_1_3_2_1_16_1","unstructured":"Microsoft. 2023. Language Server Protocol. https:\/\/microsoft.github.io\/language-server-protocol"},{"key":"e_1_3_2_1_17_1","volume-title":"Jin Peng Zhou, Christian Szegedy, \u0141ukasz Kuci\u0144ski, Piotr Mi\u0142o\u015b, and Yuhuai Wu.","author":"Miku\u0142a Maciej","year":"2023","unstructured":"Maciej Miku\u0142a, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, \u0141ukasz Kuci\u0144ski, Piotr Mi\u0142o\u015b, and Yuhuai Wu. 2023. Magnushammer: A Transformer-based Approach to Premise Selection. arxiv:2303.04488."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2023.26"},{"key":"e_1_3_2_1_20_1","unstructured":"Talia Ringer. 2021. Proof Repair. Ph. D. Dissertation. University of Washington."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373823"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_3_2_1_24_1","unstructured":"Amitayush Thakur Yeming Wen and Swarat Chaudhuri. 2023. A Language-Agent Approach to Formal Theorem-Proving. arxiv:2310.04353."},{"key":"e_1_3_2_1_25_1","unstructured":"The Coq Development Team. 2024. Coq \u2013 Release 8.19.1. https:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_26_1","unstructured":"The Coq LSP Development Team. 2024. Coq LSP \u2013 Release 0.1.8. https:\/\/github.com\/ejgallego\/coq-lsp"},{"key":"e_1_3_2_1_27_1","unstructured":"Hugo Touvron Louis Martin Kevin Stone Peter Albert Amjad Almahairi Yasmine Babaei Nikolay Bashlykov Soumya Batra Prajjwal Bhargava Shruti Bhosale Dan Bikel Lukas Blecher Cristian Canton Ferrer Moya Chen Guillem Cucurull David Esiobu Jude Fernandes Jeremy Fu Wenyin Fu Brian Fuller Cynthia Gao Vedanuj Goswami Naman Goyal Anthony Hartshorn Saghar Hosseini Rui Hou Hakan Inan Marcin Kardas Viktor Kerkez Madian Khabsa Isabel Kloumann Artem Korenev Punit Singh Koura Marie-Anne Lachaux Thibaut Lavril Jenya Lee Diana Liskovich Yinghai Lu Yuning Mao Xavier Martinet Todor Mihaylov Pushkar Mishra Igor Molybog Yixin Nie Andrew Poulton Jeremy Reizenstein Rashi Rungta Kalyan Saladi Alan Schelten Ruan Silva Eric Michael Smith Ranjan Subramanian Xiaoqing Ellen Tan Binh Tang Ross Taylor Adina Williams Jian Xiang Kuan Puxin Xu Zheng Yan Iliyan Zarov Yuchen Zhang Angela Fan Melanie Kambadur Sharan Narang Aurelien Rodriguez Robert Stojnic Sergey Edunov and Thomas Scialom. 2023. Llama 2: Open Foundation and Fine-Tuned Chat Models. arxiv:2307.09288."},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the 36th International Conference on Machine Learning. 97","author":"Yang Kaiyu","year":"2019","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In Proceedings of the 36th International Conference on Machine Learning. 97, PMLR, 6984\u20136994."},{"key":"e_1_3_2_1_29_1","volume-title":"Advances in Neural Information Processing Systems (NeurIPS","volume":"21612","author":"Yang Kaiyu","year":"2023","unstructured":"Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. 2023. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. In Advances in Neural Information Processing Systems (NeurIPS 2023, Vol. 36). Curran Associates, Inc., 21573\u201321612."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_31_1","volume-title":"8th Conference on Artificial Intelligence and Theorem Proving, Sept., arxiv:2305","author":"Zhang Shizhuo Dylan","year":"2023","unstructured":"Shizhuo Dylan Zhang, Talia Ringer, and Emily First. 2023. Getting More out of Large Language Models for Proofs. 8th Conference on Artificial Intelligence and Theorem Proving, Sept., arxiv:2305.04369."}],"event":{"name":"FSE '24: 32nd ACM International Conference on the Foundations of Software Engineering","location":"Porto de Galinhas Brazil","acronym":"FSE '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3663529.3663814","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3663529.3663814","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:21Z","timestamp":1750290261000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3663529.3663814"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,10]]},"references-count":30,"alternative-id":["10.1145\/3663529.3663814","10.1145\/3663529"],"URL":"https:\/\/doi.org\/10.1145\/3663529.3663814","relation":{},"subject":[],"published":{"date-parts":[[2024,7,10]]},"assertion":[{"value":"2024-07-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}