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 our code, including code for the PROOFWALA framework and the Multilingual ITP interaction framework. [Download paper here](https://arxiv.org/abs/2502.04671) 