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

TL;DR

ProofBridge tackles auto-formalization of complete NL theorems and proofs into Lean 4 by learning a joint NL-FL embedding that enables cross-modal retrieval of semantically relevant Lean theorems. It combines retrieval-augmented fine-tuning of a state-of-the-art prover with an iterative verifier-guided repair loop, ensuring both syntactic correctness and semantic fidelity. The approach is validated on a large NL↔Lean dataset (NuminaMath-Lean-PF) and a Lean-4 benchmark (miniF2F-Test-PF), showing substantial gains in cross-modal retrieval and proof correctness (SC) as well as type correctness (TC) over strong baselines. This framework reduces manual intervention in formalizing proofs and demonstrates the value of structured proof representations and semantic equivalence checking in formal mathematics.

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. Our training ensures that NL-FL theorems (and their proofs) are mapped close together in this space if and only if the NL-FL pairs are semantically equivalent. ProofBridge integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean's type checker and semantic equivalence feedback to ensure both syntactic correctness and semantic fidelity. Experiments show substantial improvements in proof auto-formalization over strong baselines (including GPT-5, Gemini-2.5, Kimina-Prover, DeepSeek-Prover), with our retrieval-augmented approach yielding significant gains in semantic correctness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass@k metrics on miniF2F-Test-PF, a dataset we curated. In particular, ProofBridge improves cross-modal retrieval quality by up to 3.28x Recall@1 over all-MiniLM-L6-v2, and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Prover-RL-1.7B.

Figures (4)

• Figure 1: Pipeline of ProofBridge for proof auto-formalization. We first train a joint embedding model for NL and FL via contrastive learning, enabling cross-modal retrieval of semantically related FL theorem-proof pairs for a given NL input. An LLM is then fine-tuned on NL-to-Lean translations, conditioned on retrieved proofs and relevance scores. At inference, the system retrieves related Lean proofs and applies an iterative repair loop to the generated FL theorem-proof pair.
• Figure 2: Tactic-style Proof. A Lean proof represented as a DAG of tactics.
• Figure 3: Category-wise Results. Proof auto-formalization performance across mathematical domains.
• Figure : Iterative Proof Repair