[2510.15681] ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings

Computer Science > Logic in Computer Science arXiv:2510.15681 (cs) [Submitted on 17 Oct 2025 (v1), last revised 29 Mar 2026 (this version, v3)] Title:ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings Authors:Prithwish Jana, Kaan Kale, Ahmet Ege Tanriverdi, Cruise Song, Sriram Vishwanath, Vijay Ganesh View a PDF of the paper titled ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings, by Prithwish Jana and 5 other authors View PDF HTML (experimental) Abstract:Translating human-written mathematical theorems and proofs from natural language (NL) into formal languages (FLs) like Lean 4 has long been a significant challenge for AI. Most state-of-the-art methods either focus on theorem-only NL-to-FL auto-formalization or on FL proof synthesis from FL theorems. In practice, auto-formalization of both theorem and proof still requires human intervention, as seen in AlphaProof's silver-medal performance at the 2024 IMO, where problem statements were manually translated before automated proof synthesis. We present ProofBridge, a unified framework for automatically translating entire NL theorems and proofs into Lean 4. At its core is a joint embedding model that aligns NL and FL (NL-FL) theorem+proof pairs in a shared semantic space, enabling cross-modal retrieval of semantically relevant FL examples to guide translation. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveragi...