Document Open Access Logo

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving

Authors Amitayush Thakur , George Tsoukalas , Greg Durrett , Swarat Chaudhuri

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2026.24.pdf
  • Filesize: 1.89 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
  • Computing methodologies → Machine learning
Keywords
  • neural theorem proving
  • ITP
  • automated reasoning
  • LLM guided theorem proving
  • ITP framework

Metrics

Abstract

Neural approaches to theorem proving require robust infrastructure for interfacing with interactive theorem provers (ITPs), extracting structured proof data, and executing proof search at scale. However, existing tooling is often assistant-specific and oriented toward interactive, file-level execution, making repository-scale analysis and parallel experimentation challenging. We present ProofWala, a multilingual proof engineering framework built around itp-interface, a reusable library for programmatic interaction with ITPs. For Lean 4, we implement a meta-programmed interaction layer that executes inside the elaborator, enabling semantically faithful tactic-level tracing together with declaration- and dependency-level extraction across entire repositories. This design extends beyond traditional REPL-style interaction by supporting project-wide analysis, environment cloning, and pooled execution of proof states. The implementation is robust across Lean 4 versions after 4.15.0 with forward compatibility support. The same interface abstraction supports tactic execution and data extraction for multiple versions of Rocq, yielding a unified cross-assistant pipeline.
Built on this infrastructure, ProofWala provides standardized multilingual proof datasets, model training utilities, and parallel proof search algorithms. Using the framework, we demonstrate that multilingual training across Lean and Rocq enables cross-lingual and cross-domain transfer. In particular, we observe statistically significant improvements on the largest benchmark (Lean/Mathlib) and in domain adaptation (CategoryTheory), while other settings exhibit consistent but not statistically significant trends in favor of multilingual training. We open-source the full framework, including the parallel proof search module, the itp-interface library, multilingual datasets, and trained models, providing a scalable foundation for proof mining, neural theorem proving, and cross-assistant experimentation.

Cite As Get BibTex

Amitayush Thakur, George Tsoukalas, Greg Durrett, and Swarat Chaudhuri. ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving. In 17th International Conference on Interactive Theorem Proving (ITP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 382, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITP.2026.24

Author Details

Amitayush Thakur
  • University of Texas, Austin, TX, USA
George Tsoukalas
  • University of Texas, Austin, TX, USA
Greg Durrett
  • University of Texas, Austin, TX, USA
Swarat Chaudhuri
  • University of Texas, Austin, TX, USA

Supplementary Materials

References

  1. Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, and Sanmi Koyejo. Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 104-123. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-90643-5_6.
  2. Lasse Blaauwbroek, Miroslav Olšák, Jason Rute, Fidel Ivan Schaposnik Massolo, Jelle Piepenbrock, and Vasily Pestun. Graph2tac: Online representation learning of formal math concepts, 2024. URL: https://arxiv.org/abs/2401.02949.
  3. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The Tactician: A Seamless, Interactive Tactic Learner and Prover for Coq, pages 271-277. Springer International Publishing, 2020. URL: https://doi.org/10.1007/978-3-030-53518-6_17.
  4. Pedro Carrott, Nuno Saavedra, Kyle Thompson, Sorin Lerner, João F. Ferreira, and Emily First. Coqpyt: Proof navigation in python in the era of llms. In Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering, volume 21612 of FSE ’24, pages 637-641. ACM, July 2024. URL: https://doi.org/10.1145/3663529.3663814.
  5. Alexis Conneau, Kartikay Khandelwal, Naman Goyal, Vishrav Chaudhary, Guillaume Wenzek, Francisco Guzmán, Edouard Grave, Myle Ott, Luke Zettlemoyer, and Veselin Stoyanov. Unsupervised cross-lingual representation learning at scale. arXiv preprint arXiv:1911.02116, 2019. URL: https://arxiv.org/abs/1911.02116.
  6. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378-388. Springer, 2015. Google Scholar
  7. Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve, and Amaury Hayat. ABEL: Sample efficient online reinforcement learning for neural theorem proving. In The 4th Workshop on Mathematical Reasoning and AI at NeurIPS'24, 2024. URL: https://openreview.net/forum?id=kk3mSjVCUO.
  8. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021. URL: https://arxiv.org/abs/2102.06203.
  9. Gérard Huet, Gilles Kahn, and Christine Paulin-Mohring. The coq proof assistant a tutorial. Rapport Technique, 178, 1997. Google Scholar
  10. Albert Q. Jiang, Wenda Li, and Mateja Jamnik. Multilingual mathematical autoformalization, 2023. URL: https://doi.org/10.48550/arXiv.2311.03755.
  11. Andrei Kozyrev, Gleb Solovev, Nikita Khramov, and Anton Podkopaev. Coqpilot, a plugin for llm-based generation of proofs. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, ASE ’24, pages 2382-2385. ACM, October 2024. URL: https://doi.org/10.1145/3691620.3695357.
  12. Guillaume Lample, Timothee Lacroix, Marie-Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35:26337-26349, 2022. Google Scholar
  13. Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107-115, 2009. URL: https://doi.org/10.1145/1538788.1538814.
  14. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving, 2024. URL: https://doi.org/10.48550/arXiv.2404.09939.
  15. Mathcomp. GitHub - math-comp/math-comp: Mathematical Components - github.com. https://github.com/math-comp/math-comp, 2015. [Accessed 01-06-2024].
  16. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, POPL ’20. ACM, January 2020. URL: https://doi.org/10.1145/3372885.3373824.
  17. Philipp Moritz, Robert Nishihara, Stephanie Wang, Alexey Tumanov, Richard Liaw, Eric Liang, Melih Elibol, Zongheng Yang, William Paul, Michael I Jordan, et al. Ray: A distributed framework for emerging AI applications. In 13th USENIX symposium on operating systems design and implementation (OSDI 18), pages 561-577, 2018. Google Scholar
  18. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. Google Scholar
  19. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. URL: https://arxiv.org/abs/2009.03393.
  20. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, pages 1-10, 2020. URL: https://doi.org/10.1145/3394450.3397466.
  21. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean, 2024. URL: https://doi.org/10.48550/arXiv.2404.12534.
  22. Streamlit Inc. Streamlit: A faster way to build and share data apps, 2026. Accessed: 2026-05-04. URL: https://streamlit.io/.
  23. Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An in-context learning agent for formal theorem-proving. In First Conference on Language Modeling, 2024. Google Scholar
  24. George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provers on the putnam mathematical competition, 2024. URL: https://doi.org/10.48550/arXiv.2407.11214.
  25. Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions in lean, 2023. URL: https://doi.org/10.48550/arXiv.2310.18457.
  26. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, pages 6984-6994. PMLR, 2019. URL: http://proceedings.mlr.press/v97/yang19a.html.
  27. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai, 2024. URL: https://doi.org/10.48550/arXiv.2412.16075.
  28. Kaiyu Yang, Aidan M Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626, 2023. URL: https://doi.org/10.48550/arXiv.2306.15626.
  29. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021. URL: https://arxiv.org/abs/2109.00110.
  30. Thomas Zhu, Josh Clune, and Sean Welleck. Neural theorem proving toolkit, 2023. URL: https://github.com/cmu-l3/ntp-toolkit.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact