Neural networks have shown substantial promise at automatic theorem-proving in interactive proof assistants (ITPs) like Lean and Coq. However, most neural theorem-proving models are restricted to specific ITPs, leaving out opportunities for cross-lingual transfer between ITPs. We address this weakness with a multilingual proof framework, PROOFWALA, that allows a standardized form of interaction between neural theorem-provers and two established ITPs (Coq and Lean). It enables the collection of multilingual proof step data -- data recording the result of proof actions on ITP states -- for training neural provers. PROOFWALA allows the systematic evaluation of a model's performance across different ITPs and problem domains via efficient parallel proof search algorithms. We show that multilingual training enabled by PROOFWALA can lead to successful transfer across ITPs. Specifically, a model trained on a mix of PROOFWALA-generated Coq and Lean data outperforms Lean-only and Coq-only models on the standard prove-at-k metric. We open source all code including code for the PROOFWALA Framework (https://github.com/trishullab/proof-wala), and the Multilingual ITP interaction framework (https://github.com/trishullab/itp-interface).
@article{arxiv.2502.04671,
title = {ProofWala: Multilingual Proof Data Synthesis and Theorem-Proving},
author = {Amitayush Thakur and George Tsoukalas and Greg Durrett and Swarat Chaudhuri},
journal= {arXiv preprint arXiv:2502.04671},
year = {2025}
}