DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2026.24

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

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

Published in: LIPIcs, Volume 382, 17th International Conference on Interactive Theorem Proving (ITP 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{thakur_et_al:LIPIcs.ITP.2026.24,
  author =	{Thakur, Amitayush and Tsoukalas, George and Durrett, Greg and Chaudhuri, Swarat},
  title =	{{ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving}},
  booktitle =	{17th International Conference on Interactive Theorem Proving (ITP 2026)},
  pages =	{24:1--24:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-436-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{382},
  editor =	{Komendantskaya, Ekaterina and Nipkow, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2026.24},
  URN =		{urn:nbn:de:0030-drops-269983},
  doi =		{10.4230/LIPIcs.ITP.2026.24},
  annote =	{Keywords: neural theorem proving, ITP, automated reasoning, LLM guided theorem proving, ITP framework}
}

Document

DOI: 10.4230/DagRep.7.3.27

Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)

Authors: Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge

Published in: Dagstuhl Reports, Volume 7, Issue 3 (2017)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 17111 "Game Theory in AI, Logic, and Algorithms".

Cite as

Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge. Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111). In Dagstuhl Reports, Volume 7, Issue 3, pp. 27-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{chaudhuri_et_al:DagRep.7.3.27,
  author =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  title =	{{Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)}},
  pages =	{27--32},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{3},
  editor =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.3.27},
  URN =		{urn:nbn:de:0030-drops-79609},
  doi =		{10.4230/DagRep.7.3.27},
  annote =	{Keywords: game theory, formal methods, logic, algorithms, equilibria, multiagent systems}
}

Search Results

Documents authored by Chaudhuri, Swarat

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

Abstract

Cite as

Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)

Abstract

Cite as

Thanks for your feedback!

Could not send message