{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,23]],"date-time":"2026-10-23T20:31:12Z","timestamp":1792787472457,"version":"4.5.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001475","name":"Nanyang Technological University","doi-asserted-by":"publisher","award":["Nanyang Assistant Professorship Start-Up Grant."],"award-info":[{"award-number":["Nanyang Assistant Professorship Start-Up Grant."]}],"id":[{"id":"10.13039\/501100001475","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001475","name":"Ministry of Education, Singapore","doi-asserted-by":"publisher","award":["Academic Research Fund Tier 1 (NTU Tier 1, RG18\/25)"],"award-info":[{"award-number":["Academic Research Fund Tier 1 (NTU Tier 1, RG18\/25)"]}],"id":[{"id":"10.13039\/501100001475","id-type":"DOI","asserted-by":"publisher"}]},{"name":"NSFC","award":["92582108"],"award-info":[{"award-number":["92582108"]}],"id":[{"id":"https:\/\/ror.org\/01h0zpd94","id-type":"ROR","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,4,10]]},"abstract":"<jats:p>Neural Theorem Proving (NTP) employs Large Language Models (LLMs) to automate formal proofs in proof assistants. While LLMs have achieved relatively remarkable success in informal reasoning tasks using natural languages, the transition to mechanized formal theorem proving presents persistent challenges. Mechanized proof languages often contain many syntactic constructs and diverse, specialized proof tactics, which facilitate expert use but have no direct counterpart in informal mathematical proofs. These prover-specific idioms represent an additional burden for LLM-based NTPs that might be otherwise successful in generating informal proofs. Seeking to bridge this gap between formal proof construction and informal reasoning, in order to better facilitate NTP, this work approaches these challenges from a language design perspective. We look at common reasoning patterns in informal proofs and in existing mechanized proofs, and design Minilang (formally named Isabelle\/Minilang), a minimalist proof language that captures these reasoning patterns. In contrast to proof languages (informal and formal) that often feature a large collection of operations with unclear semantic boundaries, Minilang is deliberately kept minimalist \u2013 its core design comprises only 10 proof operations, each with clear semantic distinctions. We further develop a rule-based translator from Isabelle\u2019s proof language (Isar) to Minilang, translating \u223c340,000 existing Isabelle proofs with an \u223c85% success rate. Using this translated corpus, we finetune two LLMs to compare machine learning performance on Minilang versus the original Isar language. Experiments show Minilang benefits the two LLMs by improving the pass@1 success rate on the PISA benchmark by up to 20\/29 percentage points in comparison to the Isar-based LLMs w\/wo Sledgehammer. The pass@1 rate reaches 69.1%, exceeding the prior work Baldur\u2019s pass@64 (65.7%); the pass@8 rate reaches 79.2%, exceeding the state-of-the-art on PISA (71.0%) achieved by Magnushammer.<\/jats:p>","DOI":"10.1145\/3798275","type":"journal-article","created":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T14:33:43Z","timestamp":1775831623000},"page":"2073-2098","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Minimalist Proof Language for Neural Theorem Proving over Isabelle\/HOL"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9196-3237","authenticated-orcid":false,"given":"Qiyuan","family":"Xu","sequence":"first","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0611-0755","authenticated-orcid":false,"given":"Renxi","family":"Wang","sequence":"additional","affiliation":[{"name":"MBZUAI, Abu Dhabi, United Arab Emirates"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3241-0023","authenticated-orcid":false,"given":"Peixin","family":"Wang","sequence":"additional","affiliation":[{"name":"East China Normal University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6623-5089","authenticated-orcid":false,"given":"Haonan","family":"Li","sequence":"additional","affiliation":[{"name":"MBZUAI, Abu Dhabi, United Arab Emirates"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0596-877X","authenticated-orcid":false,"given":"Conrad","family":"Watt","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"crossref","unstructured":"Tudor Achim Alex Best Kevin Der Math\u00efs F\u00e9d\u00e9rico Sergei Gukov Daniel Halpern-Leister Kirsten Henningsgard Yury Kudryashov Alexander Meiburg Martin Michelsen Riley Patterson Eric Rodriguez Laura Scharff Vikram Shanker Vladmir Sicca Hari Sowrirajan Aidan Swope Matyas Tamas Vlad Tenev Jonathan Thomm Harold Williams and Lawrence Wu. 2025. Aristotle: IMO-level Automated Theorem Proving. arXiv:2510.01346 [cs.AI] https:\/\/arxiv.org\/abs\/2510.01346","DOI":"10.70777\/si.v3i3.18745"},{"key":"e_1_3_1_3_2","unstructured":"AFP contributors. 2025. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/statistics\/"},{"key":"e_1_3_1_4_2","unstructured":"Zhangir Azerbayev Hailey Schoelkopf Keiran Paster Marco Dos Santos Stephen Marcus McAleer Albert Q. Jiang Jia Deng Stella Biderman and Sean Welleck. 2024. Llemma: An Open Language Model for Mathematics. In The Twelfth International Conference on Learning Representations. OpenReview.net. https:\/\/openreview.net\/forum?id=4WnqRR915j"},{"key":"e_1_3_1_5_2","first-page":"454","volume-title":"Proceedings of the 36th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 97)","author":"Bansal Kshitij","year":"2019","unstructured":"Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of the 36th International Conference on Machine Learning (Proceedings of Machine Learning Research, Vol. 97), Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 454\u2013463. https:\/\/proceedings.mlr.press\/v97\/bansal19a.html"},{"key":"e_1_3_1_6_2","unstructured":"Andrej Bauer Matej Petkovic and Ljupco Todorovski. 2023. MLFMF: Data Sets for Machine Learning for Mathematical Formalization. In Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023 NeurIPS 2023 New Orleans LA USA December 10 - 16 2023 Alice Oh Tristan Naumann Amir Globerson Kate Saenko Moritz Hardt and Sergey Levine (Eds.). http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/9efe8db7fab57e19eed25718abedbbd2-Abstract-Datasets_and_Benchmarks.html"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3759425.3763384"},{"key":"e_1_3_1_8_2","unstructured":"Luoxin Chen Jinming Gu Liankai Huang Wenhao Huang Zhicheng Jiang Allan Jie Xiaoran Jin Xing Jin Chenggang Li Kaijing Ma Cheng Ren Jiawei Shen Wenlei Shi Tong Sun He Sun Jiahui Wang Siran Wang Zhihong Wang Chenrui Wei Shufa Wei Yonghui Wu Yuchen Wu Yihang Xia Huajian Xin Fan Yang Huaiyuan Ying Hongyi Yuan Zheng Yuan Tianyang Zhan Chi Zhang Yue Zhang Ge Zhang Tianyun Zhao Jianqiu Zhao Yichi Zhou and Thomas Hanwen Zhu. 2025. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving. arXiv:2507.23726 [cs.AI] https:\/\/arxiv.org\/abs\/2507.23726"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09580-x"},{"key":"e_1_3_1_11_2","unstructured":"Google DeepMind. 2024. AI achieves silver-medal standard solving International Mathematical Olympiad problems. https:\/\/deepmind.google\/discover\/blog\/ai-solves-imo-problems-at-silver-medal-level\/."},{"key":"e_1_3_1_12_2","unstructured":"Isabelle contributors. 2024. HOL libraries. the src\/HOL folder in the redistribution pack of Isabelle 2024 https:\/\/isabelle.in.tum.de\/website-Isabelle2024. [Online; accessed 07-May-2025]."},{"key":"e_1_3_1_13_2","unstructured":"Albert Qiaochu Jiang Wenda Li Jesse Michael Han and Yuhuai Wu. 2021. LISA: Language models of ISAbelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving (AITP). https:\/\/aitp-conference.org\/2021\/abstract\/paper_17.pdf"},{"key":"e_1_3_1_14_2","unstructured":"Albert Qiaochu Jiang Wenda Li Szymon Tworkowski Konrad Czechowski Tomasz Odrzyg\u00f3zdz Piotr Milos Yuhuai Wu and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS 2022 New Orleans LA USA November 28 - December 9 2022. http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/377c25312668e48f2e531e2f2c422483-Abstract-Conference.html"},{"key":"e_1_3_1_15_2","volume-title":"The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda","author":"Jiang Albert Qiaochu","year":"2023","unstructured":"Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timoth\u00e9e 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, ICLR 2023, Kigali, Rwanda. OpenReview.net. https:\/\/openreview.net\/forum?id=SMa9EAovKMC"},{"key":"e_1_3_1_16_2","volume-title":"ICLR 2017, Toulon, France, April 24-26, 2017","author":"Kaliszyk Cezary","year":"2017","unstructured":"Cezary Kaliszyk, Fran\u00e7ois Chollet, and Christian Szegedy. 2017. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In ICLR 2017, Toulon, France, April 24-26, 2017. OpenReview.net. https:\/\/openreview.net\/forum?id=ryuxYmvel"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_6"},{"key":"e_1_3_1_18_2","unstructured":"Lean community. 2025. Logic and Proof. https:\/\/leanprover-community.github.io\/logic_and_proof\/introduction.html. [Online; accessed 07-May-2025]."},{"key":"e_1_3_1_19_2","volume-title":"ICLR 2021, Virtual Event, Austria, May 3-7","author":"Li Wenda","year":"2021","unstructured":"Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. 2021. IsarStep: a Benchmark for High-level Mathematical Reasoning. In ICLR 2021, Virtual Event, Austria, May 3-7. OpenReview.net. https:\/\/openreview.net\/forum?id=Pzj6fzU6wkj"},{"key":"e_1_3_1_20_2","volume-title":"The 1st Conference on Language Modeling","author":"Li Zhaoyu","year":"2024","unstructured":"Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. 2024. A Survey on Deep Learning for Theorem Proving. In The 1st Conference on Language Modeling. OpenReview.net. https:\/\/openreview.net\/forum?id=zlw6AHwukB"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695521"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9085-y"},{"key":"e_1_3_1_23_2","volume-title":"The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024","author":"Mikula Maciej","year":"2024","unstructured":"Maciej Mikula, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Q. Jiang, Jin Peng Zhou, Christian Szegedy, Lukasz Kucinski, Piotr Milos, and Yuhuai Wu. 2024. Magnushammer: A Transformer-Based Approach to Premise Selection. In The Twelfth International Conference on Learning Representations, ICLR 2024, Vienna, Austria, May 7-11, 2024. OpenReview.net. https:\/\/openreview.net\/forum?id=oYjPk8mqAV"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"e_1_3_1_25_2","unstructured":"Karl Palmskog. 2022. qarith-stern-brocot. https:\/\/github.com\/rocq-community\/qarith-stern-brocot\/blob\/9400dafdc7e35b53d23ab336e3a1b548c3b09133\/theories\/sqrt2.v. [Online; accessed 07-May-2025]."},{"key":"e_1_3_1_26_2","unstructured":"Z. Z. Ren Zhihong Shao Junxiao Song Huajian Xin Haocheng Wang Wanjia Zhao Liyue Zhang Zhe Fu Qihao Zhu Dejian Yang Z. F. Wu Zhibin Gou Shirong Ma Hongxuan Tang Yuxuan Liu Wenjun Gao Daya Guo and Chong Ruan. 2025. DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv:2504.21801 [cs.CL] https:\/\/arxiv.org\/abs\/2504.21801"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_3_1_28_2","unstructured":"Haiming Wang Mert Unsal Xiaohan Lin Mantas Baksys Junqi Liu Marco Dos Santos Flood Sung Marina Vinyes Zhenzhe Ying Zekai Zhu Jianqiao Lu Hugues de Saxc\u00e9 Bolton Bailey Chendong Song Chenjun Xiao Dehao Zhang Ebony Zhang Frederick Pu Han Zhu Jiawei Liu Jonas Bayer Julien Michel Longhui Yu L\u00e9o Dreyfus-Schmidt Lewis Tunstall Luigi Pagani Moreira Machado Pauline Bourigault Ran Wang Stanislas Polu Thibaut Barroyer Wen-Ding Li Yazhe Niu Yann Fleureau Yangyang Hu Zhouliang Yu Zihan Wang Zhilin Yang Zhengying Liu and Jia Li. 2025. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv:2504.11354 [cs.AI] https:\/\/arxiv.org\/abs\/2504.11354"},{"key":"e_1_3_1_29_2","unstructured":"Sean Welleck and Rahul Saha. 2023. LLMSTEP: LLM proofstep suggestions in Lean. arXiv:2310.18457 [cs.AI] https:\/\/arxiv.org\/abs\/2310.18457"},{"key":"e_1_3_1_30_2","unstructured":"Makarius Wenzel. 2025. The Isabelle\/Isar Implementation. https:\/\/isabelle.in.tum.de\/doc\/implementation.pdf Chapter 0 covers Isabelle\/ML. With contributions by Stefan Berghofer Florian Haftmann and Larry Paulson."},{"key":"e_1_3_1_31_2","unstructured":"Wikipedia. 2025. Isabelle (proof assistant). http:\/\/en.wikipedia.org\/w\/index.php?title=Isabelle%20(proof%20assistant). [Online; accessed 07-May-2025]."},{"key":"e_1_3_1_32_2","volume-title":"ICLR 2025, Singapore, April 24-28","author":"Xin Huajian","year":"2025","unstructured":"Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Haowei Zhang, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, and Chong Ruan. 2025. DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search. In ICLR 2025, Singapore, April 24-28. OpenReview.net. https:\/\/openreview.net\/forum?id=I4YAIwrsXa"},{"key":"e_1_3_1_33_2","doi-asserted-by":"crossref","unstructured":"Ran Xin Chenguang Xi Jie Yang Feng Chen Hang Wu Xia Xiao Yifan Sun Shen Zheng and Kai Shen. 2025. BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. arXiv:2502.03438 [cs.AI] https:\/\/arxiv.org\/abs\/2502.03438","DOI":"10.18653\/v1\/2025.acl-long.1565"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","unstructured":"Qiyuan Xu and Renxi Wang. 2026. Artifact: A Minimal Proof Language for Neural Theorem Proving over Isabelle\/HOL. doi:10.5281\/zenodo.18454706","DOI":"10.5281\/zenodo.18454706"},{"key":"e_1_3_1_35_2","first-page":"6984","volume-title":"Proceedings of the 36th International Conference on Machine Learning","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, Vol. 97. PMLR, 6984\u20136994. https:\/\/proceedings.mlr.press\/v97\/yang19a.html"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2024.acl-demos.38"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3798275","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T11:23:25Z","timestamp":1790421805000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3798275"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,10]]},"references-count":35,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2026,4,10]]}},"alternative-id":["10.1145\/3798275"],"URL":"https:\/\/doi.org\/10.1145\/3798275","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,10]]},"assertion":[{"value":"2025-10-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-02-17","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}