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
Venue: ICLR 2026 Poster (2026)
Keywords: proof auto-formalization
mathematical theorem proving
Lean 4 interactive theorem prover
joint embedding
cross-modal retrieval
large language model (LLM)
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)
TL;DR: ProofBridge is a unified framework that translates natural language theorems and proofs into Lean 4 using joint embeddings, cross-modal retrieval-augmented fine-tuning, and iterative proof repair, achieving strong semantic and type correctness gains.

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, 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.

Published as a conference paper at ICLR 2026
PROOFBRIDGE: AUTO-FORMALIZATION OF NATURAL LANGUAGE PROOFS IN LEAN VIA JOINT EMBEDDINGS
Prithwish Jana"l, Kaan Kale', Ahmet Ege Tanriverdi
Cruise Song', Sriram Vishwanath', Vijay Ganesh"
GGeorgia Institute of Technology, USA
Bogaziei University, Türkiye
ABSTRACT
mathematical theorems and proofs from natural lan- guage (NI.) into formal languages (FI.s) like Lean 4 has long been significant challenge for AI. Most state-of-the-aa methods either focus on theorem-only NL- to-FL fontaloommaiiztiion 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.
Translating
We present PROOFBRINGE, 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 shared seman- tic space, enabling cross- modal retrieval of semantically relevant FL examples guide translation. PROOFBRIDGE integrates retrieval-augmented fine-tuning with iterative proof repair, leveraging Lean's type checker and semantic equiv- alence feedback ensure both syntactic correctness and semantic fidelity. Ex- periments show substantial improvements in proof fortoofomalizziionn over strong basclines (including GPT-5, Gemini-2.5. -rovvr,, DeepSeek- Prover), with our retrieval-an -aggeendd approach yielding significant gains in semantic correct- ness (SC, via proving bi-directional equivalence) and type correctness (TC, via type-checking theorem+proof) across pass @ metrics on MINIF2F-TEST PF, dataset we curated. particular, PROOFBRIDGE improves cross-modal retrieval quality by to 3.28x Recall@) 1 over M-I-Minn and achieves +31.14% SC and +1.64% TC (pass@32) compared to the baseline Kimina-Proved Prover-RL-1.7B
INTRODUCTION
In mathematics, ensuring the correctness of proofs a crucial yet inherently difficult task. Tradi- tionally, mathematicians rely the peer-review process for proof verification, yet proofs grow increasingly complex, even careful human scrutiny can overlook subtle errors. For instance, in 1989, Kapranov and Voevodsky published proof connecting co-groupoids and homotopy types, which was later disproven by Carlos Simpson in 1998; more recently, while formalizing his 2023 pa- per (Tao) 2023) on the Maclaurin-type inequality, Terence Tao discovered non-trivial bug. To mit- igate challenges of verifying complex proofs, proof assistants and formal mathematical languages like Isabelle (Nipkow et al. 2002). HOL Light (Harrison) (009). Metamath (Megill & Wheeler 2019), Lean 4 (Moura & Ullrich 202T), Peano (Poesia & Goodman 2023), and Rocq (Sozeau et al., 2025) have been developed, offering a way to create computer- verifiable formal proofs. Such for- mal language (FL) proofs, defined by strict syntax and symbolic logic, enable reliable automated verification guarantees that resolve the inherent ambiguity of natural language (NL) proofs. How- ever, constructing FL proofs is time-intensive and demands both deep mathematical expertise and detailed knowledge of the language and its librarics. Thus, the process remains challenging even for experienced mathematicians, limiting the wider adoption of formal proof assistants and FL. proofs.
To simplify the task of writing proofs in FL, two key research directions have emerged: auto- formalization and automated formal proof synthesis (AFPS). fomalizrmaii targets NL-to-FL
translation, but most prior works (Wang et al. 2025 Wu et al. 2026 Jiang et al.) 2024 Gao et al.
"Co-corresoonding authors. Emails: (pjana7, vganesh)

---

Published as a conference paper at ICLR 2026
NUFL Contrastive Loss (4)
INL RicoIst-pootttaa pwteeppooooaaa pa10
MAi
NL Encoder (f)
O
My. (Pis AL NL Feorenssood
Enooder (o)
Joint Embbedding
Shared Semantic
Space
Mit (Less
With Pi / (Mal)) wettff. a (M!!) j sel gret
sin PRL-1) (TL hag (tve pai))
Instance
Instance
sim (e sinfr Min are melow kor pains)
(a) Joint embedding NL and (Lean) theorems and proofs into shared semantic space
Pi
Mis
Eacaderie)
My
O
Mig
SFTTrainer
MiL
Exssdercg)
Largo Dantocii
Stane Somtnti Space
Tpp virvet
Enerpy
H. Excader
(f)
pers & sore
PRoOrEROCG
Mus Leri
Miroooreraaoo pai)
(b) Retricval- augmente Supervised Fine-Tunne Tuning (SFT) of PROOFBRIDGE with NL/FL cross- moddl retrieval
Foedback hon Syrzocic Semants
NLFL Retrieval
MiL
Ventiaatio
LEVN typs (oc
Gemini Meco Frtsiin yMau???
Top Koderent thereepgroof
PROOFBRIDGE
Loop
(Tau teceemeoooo pam
LLM
MyL (Generaled
(c) Inference phase of retrieval -aggeveeeeugmeeeedddd proof auto-fonee cutto-formalization with iterative repair
Figure 1: Pipeline of PROOFBRIDGE for proof auto-formalization. We first train joint embed- ding 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 relevant Lean proofs to guide FL theorem+proof generation and applies an iterative repair loop.
focus only on formalizing theorems (statements), not proofs. In contrast, AFPS (Ren et al. Wang et al. 2025) aims to generate FL proofs given an FL theorem. Proof nottlloommaizztionn Ciang et al. 2023) for Isabelle and FormL4 (Lu jet al. 2024) for Lean serving as notable examples. In practice, formalizing an entire NL proof requires first performing theorem-only auto-formalization to translate the NL theorem into FL, fol- lowed by AFPS to generate the FL proof. AlphaProof (Deepmind 2024), which achieved silver- medal standard in the 2024 International Mathematical Olympiad, followed this two-step process: problems were manually formalized before automated proof synthesis. Thus, in practice, pipelines still require manual theorem formalization prior to proof synthesis, despite advances in theorem- only auto-forme nutto-formalizttoon and AFPS tools. This illustrates the broader challenge that current systems often rely on human intervention to ensure semantic correctness of proof tottoofommliiatiin.
2025
2025
re relatively less explored, with
Contemporary LLMs face several challenges that limit their effectiveness for proof auto- formalization in Lean 4. First, large-scale datasets pairing NL theorems with Lean 4 proofs are scarce. Most existing resources (Goedel-Pset-vl (Lin et al.) (025), Herald-statements (Gao et al. 2025). Lean Workbook (Ying et al. 2024), MMA (Jiang et al. (004)) cover only theorems, while those with proofs (Herald-proofs, Lean Workbook proofs (Lin et al. (2025). and FormL4 (Lu al., 20244) are much smaller and do not align with the popular miniF2F (Zheng et al., 2022) bench- mark in the same Lean 4 version. Lean versions are not backward compatible, cross-version
2

---

Published as a conference paper at ICLR 2026
evaluation often fails. Second, reneral-purposs foundation models often fail to satisfy strict syn- tactic and semantic constraints of specialized FLs (Jha et al. 2025; DeLorenzo et al. 2025 Jana 2024 Ugare et al.; 2024), such Lean, and are computationally expensive (Dasgupta al. 2025), motivating smaller specialized models. However, most fine-tuned L.MS for Lean target either the- orem nuto-formalization proof synthesis. Proof nuto-ooomalization is harder, as it requires both translating the NL theorem and constructing the corresponding FL proof. Third, Lean 4 has an effectively infinite action space (Poesia & Goodman 2023), where proofs use complex tactics that reuse prior theorems or introduce new variables. Prior work generates FL directly from NL while ignoring semantic relations such as shared tactics and DAG dependencies, often leading LLMs to produce hallucinated or invalid proofs. Fourth, automated evaluation is major bottleneck. Lean's type-checker verifies the FL proof but cannot ensure semantic equivalence. Existing methods often type-check only the theorem (leaving proofs incomplete using placeholders like sorry) or rely on proxies such as BLEU, which are unreliable (Lu et al. 2024; Ying et al. 2024; Wu et al. 2022).
Key Insight. In this paper, we address the task of proof auto-formalization, focusing Lean 4 as the FL, via a combination of a joint embedding model, an LLM, and Lean for verification. It takes as input NL theorem+proof pair and produces the corresponding FL theorem+proof pair in Lean 4. The key insight behind our approach is to treat proof auto- formalization as learning from demon- strations: the L.M is guided not only by the NL proof but also by FL proofs retrieved using an NL/FL joint embedding model that leverages contrastive learning and encodes linear DAG traver- sals of Lean proofs. Rather than relying on randomly chosen few-shot examples, these retrieved proofs capture far richer reusable formalization patterns (tactic choices, DAG structures), providing grounded signals that guide generation toward -eri-verifiable proof', as illustrated in Figure
Contributions:
The PROOFBRIDGE Auto-formalization Method and Tool: We present PROOFBRIDGE, an LLM-based, retrieval-augmented proof fottaliommiiiiiionn framework. At its core is an NL/FL embedding model that maps semantically equivalent NL and FL theorem+proof pairs to nearby points in shared space, enabling rross-modal retrieval of related FL proofs. We then fine-tune the SOTA LLM P conditioned on the retrieved FL proofs and their relevance scores. During inference, generation is refined with an iterative verifier-uided repair loop combining Lean type-checking with LLM- bi-directional equivalence proving ensure syntactic correctness and semantic fidelity. (Section 4
(Wang et al., 2025) to perform NL-to-Lean 4 proof translation,
NUMINA MATNNAMAT--LEAPPP Dataset: We curate NUMINAMATH-LEAN-PP a large-scale dataset of 38.9k NLe-LLean 4 theorem+proof pairs, specialized for proof futoo-ormmlizzation. Each Lean theorem+proof pair is type-checked and paired with an NL counterpart. Additionally, we release MINIF2F-TEST-PF. Lean v4.15.0 version of miniF2F-Test with 244 instances tailored for proof auto-formalization. enabling a consistent pipeline in the same Lean version. (Section 5.1)
Extensive Experimental Evaluation: Compared to the baseline encoder Wi--Mini-.-----22 PROOFBRIGGE'S cross-modal NL. retrieval achieves 3.28x higher Recall Rate @ K at K=1 and 2.74x MRR, with top-K retrieved embeddings 23% closer and non-retrieved 104% farther. We evaluate PROOFBRIDGE against 13 SoTA LLMs, including foundation models (Gemini-2.5, GPT- 5-mini) and automated proof synthesis LLMs (DeepSeek-Prow -rrvvrr, STP, Leanabell-Prover Kimina- Prover), using verifier- rrefiee-groonded metries: rype correctess (TC) and semantic correctness (SC, new metric based on Lean bidirectional equivalence proofs). Built on
PROOF- BRIDGE achieves +31. 34% SC and +1.64% TC (pass@32) 32) on MINIF2F-TEST-PE. (Section 5
2 RELATED WORK
Our work lies at the intersection of three key Al-for-Math research areas: automated formal proof synthesis, futolfoomalization, and cerienal-augmented learning for mathematical reasoning. We focus on the most relevant approaches and highlight differences from unified framework.
Auto-lormaiization Auto-formalization translates NL mathematics into FL, but most existing work focuses on theorem formalization rather than proofs. Theorem-only approaches include Herald-translator (Gao et al., 2025). which extracts FL theorems from Mathlib4 and trains on informal counterparts, and Autofommlllr (Wang et al. 2025), which fine-tunes models with expert iteration. These excel at translating theorems but cannot handle proofs. Proof auto- formalization has received limited attention. Draft-Sketch-Proow (Tiang al. 2023) converts NI.
3

---

Published as a conference paper at ICLR 2026
proofs into formal sketches in Isabelle with open conjectures, then fills gaps using predefined tactics and tools like Sledgehammer (Paulsson & Blanchette 2010). FormL4 (Lu et al. 2024) trains on GPT-4 informalized Mathlib proots with
step-level Lean compilation feedback. Key Differences: Our approach is the first to jointly learn representations for NL and FL theo- rem+proof pairs, enabling cross-modal retrieval to guide formalization. Unlike prior work, we leverage semantic relationships of NL and FL proofs for contextual guidance.
Automated Formal Proof Synthesis (AFPS). In this setting, given FL theorem, the goal is to generate its FL proof. Next-Tactie Prediction (NTP) methods predict each proof step from the cur- rent proof state. Examples include GPT-f (Polu & Sutskever 2020) for Metamath, LIsa (Jiang al.) 2021) for Isabelle, and PACT (Han et al. (202)) for Lean. They use tree search over proof states, prioritizing tactics by cumulative probability. While NTP ensures stepwise correctness via interac- tive theorem-prover verification, it suffers from long-horizon dependencies and repeated verification overhead. Whole-Proof Generation (WPG) methods generate complete FL proofs in a single pass, offering computational efficiency but risking cascading errors. Recent advances include DeepSeek- Prover-v1 (Xin al. 2024a), which combines SFT with expert iteration, and Theoreml (Wang) et al., 2024b). which improves in-context learning via curriculum- based training. DeepSeek-Proved v2 (Ren et al. 2025) integrates NL reasoning with FL proof generation, while Kimina- Prover (Wang al. 2025) applies reinforcement learning with compilation-basel rewards (Jana al.) 2024).
Key Differences: Unlike AFPS approaches that assume FL theorems as input, our work addresses the more challenging task of generating theorem+proof pairs in FL from an NL input.
Retrieval-Augmentee Learning for Mathematics. Recent work has explored retrieval-augmeened mathematical reasoning, though not specifically for auto- auto-formalization TLAPS (Zhou 2025)
trieves verified proofs to aid proof generation, while COPRA (Thakur et al. 2024) and REAL- Prover (Shen al. 2025) retrieve lemmas or theorems to guide proof search. These methods rely on plain-text encoding. LeanSearch (Gao et al. 2024), HERALD (Gao et al. 2025), and RAutofor- malizer (Liu al., 2025) also use plain-text encoders for FL theorem retrieval: however, as shown in Section 5.5 this does not extend to the more demanding task of FL theorem+proof pair retrieval.
Key Differences: Our joint embedding enables NL/FL cross-modal retrieval of theorem+proof pairs and encodes the DAG structure of Lean proofs, unlike plain-text encoders. Capturing proof-structun semantics is essential for proof fomalaaomaiiztioon and not addressed by existing tool-chains.
Positioning our contributions. The combination of joint embedding, retrieval augmentation, and unified translation distinguishes PROOFBRIDGE from prior work: (a) Unified Proof Auto- Formalization: We address complete translation (theorem proof) rather than treating theorem formalization and proof synthesis separately.
(b) Joint Semantic Embedding: Our contrastive learn- ing framework for aligning NL and FL proofs is novel, enabling effective rross-modal retrieval. (c) Retrieval Retrieval-Augmentte Translation: We are the first to apply surieval-augment
fine-tuning and gen- eration to anto-formalization, leveraging semantic relationships of FI. proofs guide translation. (d) Rigorous Evaluation: We introduce systematic metrics for proof auto-formalization, covering type checking and semantic correctness via bi-directional equivalence proofs instead of proxy measures.
3 PRELIMINARIES: TACTIC-STYLE PROOFS IN LEAN
Lean (Moura& & Ullrich 2021 is functional programming language and interactive theorem prover that is based on the propositions-as-yy constructing a term of the corresponding type. Rather than building these terms manually, users write proofs in a tactic language, which provides high-level steps to guide term construction. Lean 4 (henceforth Lean) represents tactic-style proofs as directed acyelic graphs (DAGs) of proof states and factics, automatically generating the corresponding proof term in the background. The kernel then verifies the term, ensuring correctness by enforcing the axiomatic foundations of Lean's logic, the Calculus of Inductive Constructions. This combination of a formal system and small, trusted kernel provides strong confidence in the validity of proofs. In the DAG (Figure 2 of a Lean proof:
principle, where proving proposition is equivalent to
Each proof state S; = [G1. Gn] consists state So has goal, the theorem TEL pr F itself. Leaf-level states have open goal. Each open goal G; = pr; H en, of a proof state represents a proposition en, that needs to be proven, given of premises pr.-
sequence of zero or more open goals. Initial
4

---

Published as a conference paper at ICLR 2026
Each tactic rac; represents a proof step. is high-level command (rooted in metaprogramming) applied to an open goal Gg producing a new proof state. If the resulting proof state has no open goal, it directly resolves the current goal. A parent goal is resolved once all subgoals are resolved.
Tactic-style proof synthesis in Lean follows sequential de- cision process. Lean provides an interactive REPL (Lean- prover 2025) that applies tacties step by step manipulate proof states. An FL proof is a sequence of tactics, and at each step, the REPL updates the proof state if the tactic is valid or returns an eπrоr identifying the faulty one. Each tactic advances the proof by breaking the current goal into simpler subgoals, similar to the 'suffices to show' construct.
Proot: Pr. m [taq tacy, tao...
G2
tac.
CBC
tac
tsq
Proof Auto-formalization as Learning Problem. Given an NL theorem+proof pair Msl- (TNL, PNL). the goal is learn function f: MNL + MML that produces a cor- responding Lean theorem+proof pair MF. = (TF.,, Pr.)) Here, TF. = pr en denotes the formal theorem, and sequence of
taOys
Initill
(backward proving)
Statelsk:
The
No more
Figure 2: Tactic-style Proof. A Lean proof represented a DAG of tacties.
PFL = (taco..... tacn-1) is the proof tactics. The generated pair must satisfy:
(a) Type correctness: MF. = (TFL, PFL) passes Lean type-checking, ensuring that PFL proves TEL with no open goals in the DAG.
(b) Semantic correctness: FL theorem is semantically equivalent to the NL one, i.e., TEL = TNL.
OUR APPROACH AND TOOL ARCHITECTURE
4.1 JOINT EMBEDDING OF NI AND LEAN PROOFS FOR CROSS-MODAL RETRIEVAL
A core component of our framework is the joint embedding model, which learns to represent NL theorem+proof pairs and their FL (Lean) counterparts in shared semantic space. The goal is to align these modalities so that cross-modal retrieval between NL and FL becomes possible. Let MEL (TrL) p(f)) denote an FL theorem++pooff pair, and let D {
[1) J.M be large database of such pairs. Given an NL theorem+proof pair MNL, the model retrieves a subset R(MNL. D) D of size K < 'D] that serves as in-context demonstrations to guide downstream auto- cuttoffrmmlization.
During training, (i and Mii are encoded into vectors by modality-specife encoders. Each en- coder is initialized with pre-trained model, and a subset of parameters is subsequently fine-tuned. The NI. encoder f maps ( vector (t) UNL. (ML,, 0f(( E Rdd and the FL encoder g FL lyllog) Rd, where and á denote frozen and trainable parameters, respectively, and is the shared embedding dimension. The details of each encoder are as follows:
maps M(( to OFL
(8) = (
(i)
NL encoder f (i 0yl( To encode ML
1-1-MiniLM-L6--- Reimers & Gurevych 2019). a lightweight model (22.7M parameters) that effectively captures semantic sim- ilarity in NL. It encodes M into 384-dimensional embeddings, thereby projected into the joint embedding space of dimension d = 512 via a linear layer included in the trainable set ór. (t)
FL encoder g (M 0g [g);: Given M (1) (I p(()) first extract the linearized DAG
traversal of tactics from pf2 using Lean REPL (Laanprvver 2025). This traversal represented ordered sequence of proof-state transformations induced by successive tactic applications:
tacH-1, Sμ, where So = T(() each S₁ = [G Gi] denotes proof state consisting of zero or more open goals, and tack-1 is the tactic applied at step h. This sequence captures the entire proof as an ordered series of state transformations. To create embeddings for the full proof, we first encode each state S₁ using LeanDojo's ByT5 proof-state encoder (Yang et al. 2023) (218M parameters), producing embeddings of size 1,472 per state. We then obtain a single embedding for the entire proof via mean- srean-nooling. which is subsequently projected into shared semantic space of dimension d 512 using a linear layer included in the trainable parameters dg. The intuition behind this approach is to ensure that semantically similar proofs (those with similar DAG structures of proof states and tactics) produce similar embeddings.
So tace S tacl,
5

---

Published as a conference paper at ICLR 2026
Contrastive Learning. To enable cross-modal retrieval between NL and FL representations, it is essential to align the two modalities in the embedding space. Specifically, for each positive pair (NNT. 2F..)
(MiT. (6)), aim for their embeddings (1 (f)) to exhibit high cosine similarity, while em- beddings of mismatched pairs are pushed apart. Denoting l2 fg-normalization by 1 w/||o/l2 and defining the cosine similarity between two embeddings and w as [ū, wi, we adopt the following
symmetric contrastive loss for mini-batch B (M NL: M( Ti=1 of NL and FL pairs:
1 2n
10
exp NL.
FFL (i)
FL NNL (T) E exp
expl
) (I)
C(B)
log
+ log
سj= exp UN.. FT.. /TT
( T.. 1/T)
where 7 > O is a temperature hyperparameter. This loss encourages each NI embedding to be closest to its corresponding FL. embedding, and vice versa, using other in-batch embeddings as negatives. The negatives are sampled randomly for each mini-batch.
) [2] and NL/FL Cross-Modal Retrieval. We precompute the normalized embeddings N'N.J i=1
(=1 for all NL and FL theorem+proof pairs respectively in our database D. which enables efficient cross-modal retrieval. Given query theorem+proof pair either source modality (NI. or FL.), we encode it into the shared semantic space (yielding INL or (FL) and compute cosine similar- ities with all items in the target modality, producing the set {[NNL. [(0] [P]
j=1 or [[ĀrL. [ D depending on the retrieval direction. The top-K nearest neighbors from these sets are then selected as demonstrations, reflecting similar proof structures, patterns, and mathematical domains.
4.2 RETRIEVAL-AUGMENTT FINE-TUNING FOR PROOF AUTO-FORMALIZATION
We fine-tune LLM translate NL proo pairs into FL (Lean), conditioned retrieved FL demonstrations that provide rich contextual knowledge. For each training instance, we con- struct prompt containing (a) input NL theorem++proff pair MN1. and (b) top-K retrieved FL the- orem+proof pairs: R( D) = (M(()) lk=1 with relevance scores [r(*]] The retrieved ex- amples demonstrate how similar mathematical concepts and proof strategies formalized in Lean. We include relevance scores to help the model weight the importance of each retrieved example.
Ik=1-
Training Objective. We fine-tune Kimina-Prroer-RL--I.. learning on our NUMINAMATH-LEAN- dataset (details in Section 5.1). The model is trained to
(Wang al. 2025 using supervised
generate FL theorem+proot pair MFL given the input context. This retrieval-ause -arimeee- approach allows the LLM to learn from similar formalization patterns rather than generating formal theorems in isolation. As illustrated in Figure lb. use the standard rugr-segres language modeling loss:
IT
LCE
log Po (Te Tee,
where T = -MM is the generated formalization tokenized as sequence (TI...., TTT). ). C represents the input context (NL theorem+proof and retrieved FL examples), and 0 are the LLM parameters. This corresponds to the cross-entropy loss between MR. and the gold-standard formalization MFL.
4.3 ITERATIVE PROOF REPAIR WITH VERIFIER FEEDBACK
During inference, we perform retrieval-augmented proof coto-formalization with the fine-tuned LLM (Figure [cp. However, LLM being stochastic model may still generate FL proorem+proof pair that contain syntactic erгоrs or semantic misalignments with the input NL theorem+proof. To address, we implement an iterative repair mechanism that combines Lean's type checker with se- mantic equivalence verification. For an input NL theorem+proof pair MsL (TNL, PNL) the LLM generates an FL counterpart MRL (TF.. PFL.). which we perform types of verification:
1. Syntactic Verification:
We compile Mr.. using Lean's type checker. If compilation fails, we extract the specific error message and location from Lean's diagnostic output.
Semantic Verification: We assess whether the generated theorem TFL accurately represents the original NL theorem TNL using an LLM--bssed equivalence judge.

---

Published as a conference paper at ICLR 2026
Algorithm 1 Iterative Proof Repair
Repair Process. When either syntactic se- mantic verification fails, we initiate an iterative repair process. The procedure terminates once both checks succeed or the maximum numher
Input: NL theorem-proof peir Maa = (Thu, Psa.).
Initial FL thcorem-proof pair MR. (Tx.. ((0)
Output: Veritied theorem-proof pair or FAILURE
3 for i = O Rmax 1 do
4 symaaOO < LeanTypeCheck (ML)
of repair attempts ( (Rmax = 5) is reached. This bounded, iterative strategy improves the relia- bility of proof fotmalarmaiintioon by catching and correcting common errors while maintain- ing computational efficiency. The overall pro- cess is described in Algorithm
semanticsOK SemaaticEiqivaaeecce (TxL. TR.
6
if SyniaxOK A semanticsOK then return Ma.
feedback
Fedeenneeeodhhhcssstttte SemanticsOK)
12 4- L. L...Repirr (eedback)
end for
10 return FAII FAILUUR
EXPERIMENTAL EVALUATION
5.1 DATASETS AND PREPARATION: NUMINAMATH-LEAN AND MINIF2F-TEST-PE
For training, we construct NUMINAMAATIILLEN-PP from NuminaMath--EAN (Wang et al. 2025). containing 104, 155 competition- problems in algebra, geometry, number theory, combinatories, and calculus. Each instance pairs an NL theorem TNL with a human- -wrtten Lean v4.15.0 the- orem TFL: 38,951 include FL proofs PFl (30% (TNL. (T.., }. Next, we prepare NUMINAMATH-LEAN PF via the following steps:
rest by KiminaProver)), forming
Formal Verification and Repair. Each (TFL, PFt.) is type-checked using Lean REPL (Leanprover) 2025). About 6% (2.337) failed due to syntax, library mismatches, or incomplete proofs. These were automatically repaired via Gemini-2.5- Lean, used to prompt the LLM for corrections, and re-verified iteratively up to five times.
error messages and locations are extracted from
NL Proof Generation. As NuminaMath-LEAN provides only theorems, we generate NL proofs in two stages, First, solution sketch retrieval searches for TNI. in NuminaMath 1.5 (Li et al. 2024) (896k problem-solution pairs), retrieving NL solution sketches (median 79 words) for 25,79 25,792 in- stances (66%). Next, FL-to-NL informalization uses Gemini-2.5-PP to translate PFL into NL proofs, using available sketches, yielding 38,951 NL-FL theorem+proof pairs { (TTN,,PNL) (TFL, PrL)
For validation, we curate SAN-FFFFTEST--- by combining two versions of miniF2F-test (Zheng et al. 2022), , a widely-used auto-formalizatio benchmark. It contains 244 Olympiad-level problems from the AIME, AMC,, IMO, and undergraduate courses in algebra, number theory, and inequalities. We use the Lean v4. 15.0 version (NuminaMath) 2025) and add missing NL proof' from Yang 2025).
5.2 EVALUATION METRICS
Metrics for NL/FL Cross-Modal Retrieval. We evaluate cross- cross-moda modal aligument of our joint em- bedding model in two directions. NL + FL measures retrieval of FL theorem+proof pairs given an NL input, which is relevant for proof nuto-foomalization, while FL. -> NI. assesses the reverse. For a test pair (MsL. Mn.). retrieval in the NI. -> FL. direction is deemed successful if the model retrieves the FL counterpart MFL given MNL. and unsuccessful otherwise; the FL - NL direction is evaluated analogously. We assess retrieval performance using five metrics. (i) Recall Rate @ K measures the percentage of queries for which the query's cross-modal counterpart ap- pears among the top-K retrieved results. We report K 1, 5. 10, 20, 50. (ii) Mean Reciprocal Rank (MRR) is the average reciprocal rank of the retrieved cross cross-modal counterpart for each query, _
MRR N Eg= rank,' indicating how highly it is ranked. (ii)) Cosine Similarity of Top- K Retrieved measures the cosine similarity between the query embedding and those of the top- re- trieved instances. For each query, we sort these scores in ascending order and record three statistics: median (M), 25th percentile (Q1), and th percentile (Q3), and report their average over the test set. (iv) Cosine Similarity of Non-Retrieved applies the same procedure to all non-retrieved instances and reports the median (M), 25th percentile (Q1), and 75th percentile (Q3) averaged over the test set. (v) mean Median Gap (mMG) measures the difference between the median (M) cosine similarity of top-K K retrieved and that of non-eetreeved instances, averaged over K = 1, 5, 10, 20, 50.
Given MNL (TNL; PNL). a proof auto formalzeer gen- erates an FL version Mn. = Pr.). We evaluate this using two metrics: (i) Type Correctness (TC) checks if Mr. passes Lean's 's type-checker, i.e., Pti. proves TFL without using keyword sorry.
Metrics for Proof Auto-Formalizatinn
7

---

Published as a conference paper at ICLR 2026
(ii) Semantic Correctness (SC) is measured only for type-correct outputs and checks whether TpL is definitionally equal to TEl (we admit some propositional equalities) by prompting Gemini-2.5- up to five times to produce a Lean proof of the bi-directional equivalence Tr. t> Tr. using a stricted set of tactics, e.g., rf1, simp, ri ring etc. (see Appendix [A.4] for details). Although relying on an LLM judge, correctness is determined via the Lean proof, not the L.M's judgment alone. TC and SC are reported as pass @ k, i.c., over the top-k generated candidates, for A: 1, 16, 32.
5.3 STATE-OF-THE-ARE BASELINES
SoTA for NL/FL Cross-Modal Retrieval To our knowledge, no existing model jointly embeds theorems and proofs in NL and FL.. Pre-trained encoders alone do not yield embeddings suitable for meaningful cross-modal retrieval. To illustrate, we evaluate two SoTA Encoders: Qwen3- Embedding-SPi (Zhang et al., 2025b) and ES5-Mistral77B-Inst allows user-defined output dimensions up to 4096, and we use 512 to match our joint embedding model. while E5-Mistral (used by LeanSearch-PS (Shen et al., (025)) has a fixed dimension of 4096. We also include a Baseline Encoder, all- al--MiniLM--L6-22 (Reimers & Gurevych 2019), used for the NI. encoder in PROOFBRIDGE, producing 384-dim embeddings. All these encoders treat theorem+proof pairs as plain text, ignoring the DAG structure of FL proofs, which PROOFBRIDGE explicitly leverages. Retrieval is performed via cosine similarity in the respective embedding spaces.
(Wang et al.) 2024a). Qwen3
SoTA Tools for Proof Fumallormalization. Existing proof auto- fommalfommiiioioon tools include DSP (Jiang et al.] 2023), which supports only Isabelle, making comparison infeasible since we target Lean 4. Another recent tool, FormL4 (Lu et al.) 2024), has not yet released its trained model. We therefore compare three categories of tools. First, we consider four foundation models, includ- ing GPT-5-mini (OpenAl| 2025) and the Gemini-2.5 variants, Flash-Lite, Flash, and Pro (Comanici et al. 2025). Next, we evaluate seven AFPS LLMs that generate FL. proofs with tacties: DeepSeek- Prover-Vi.5-RL (Xin et al., 2024b), STP _TP_mdel Lean_ can_0320 (Dong & Ma (025). Goedel-Prover- SFT (Lin et al.] 2025), Leanabell-Prover- V2-KM (Zhang et al., 2025a), and three Kimina-Prove variants (Wang et al. 2025) (RL-1.7B, Distill-SB, 72B). Finally, we evaluate two auto-formalization (Wang et al., 2025) and Herald-Translatt (Gao et al. 2025)
LLMs:
5.4 TRAINING AND EVALUATION SETUP
We train our joint embedding model 90% (35,056 instances) of NUMINAMATH--EANT and evaluate it on the remaining 3,895 instances. The split is domain-stratified across all mathematical areas, ensuring hard negatives in the test set. The train split serves database D of FL the- orem+proof pairs. PROOFBRIDGE, built on Kimina-Prover--I--11PP is SFT-tuned for NL-to-FI. translation using (MNL MFL from NUMINA trieving the top-5 relevant FL proof's from D for time iterative proof repair is applied, and the model is evaluated on MINIF2F-TEST-B See Appen- dices A.3 for implementation and training details, and Appendix A.5 an example inference.
with the joint embedding model re- SFT and inference. Inference-
The SoTA Tools are evaluated in three settings: (a) zeoo-shot, with no in-context I/O examples; (b) random few-shol, with five randomly selected in-context examples; and (c) text-based retrieval few- shot, where the top-5 FI. thoor pairs are retrieved from D via Qwen3-Embedding paired with their NL counterparts as in-context examples. Further, setting: theorem-onje only formalzerr (TI) first translates TNI. to TFL and AFPS LLM (T2) then generates (TFL. PFL.) from Ti., both in zero-shot. For pass@ k, we sample the top-k from TI, select one that is TC: and judged equivalent to TNi. by Gemini-2.5-Pa (SC is not used as the gold TEL is withheld until the pipeline finishes), and then generate the top-k proof candidates from T2.
and evaluate a SoTA Two-Step
5.5 EXPERIMENTAL RESULTS
NL/FL Cross-Modal Retrieval. Table I compares PROOFBRIDGE's joint embedding model with the two SoTA Encoders and the Baseline Encoder. Since PROOrBRIDGE is obtained by contrastively training the NL encoder together with an FL encoder, all improvements are reported relative to the original NL encoder (the Baseline Encoder). PROOFBRIDGE achieves consistently higher recall rates across all top- values: for NL- it yields 3.28x gain for NL-FL and 1.94x for FL-NN at K = 1. MRR also improves by 2.74x and 1.79x for NL. and FI.+NL, respectively. This
8

---

Published as a conference paper at ICLR 2026
Table 1: NL/FL Cross-Modal Retrieval Performance. Retrieval performance of SoTA and Base- line encoders versus PROOFBRIDGE'S ' joint embedding. (01: 25th atile, M. median, Q3: 75th %tile)
Methaad
Netriena
Recall Rate @ K
Cas. Similarity tftep-K Retriered
Co.. Similarity NOT Retriered
Gap (mMG)
Kel
Keb
Kei0
K=20 K=50
Kei
Kob
Km10
K=20
K=50
Keb
K=10
K-20
K=50
0.34
0.67
0.62
0.50
0.57
0.317
0.317
0,517
0.74
0.63
0.22
0.38
0,362
0,362
0.361
0.362
0.352
Quees Brbbeddag BB NL. BL 46.05 21.66
82.59
37.M 90.34
05:
0.74
0.70
0.66
0.65
0.50
0.410
0410
0.40
0.409
0,800
1.29
(8:77), Enssier, NB parom))
0.76
0.76
1167
0.06
0.63
0163
0.63
0.310
0.301
0.662
0.309
0.563
0,309
01.00
NL-NL
69.26
29.79
$3.78
$7.36
0.506
0.30
03:
0,86
0.53
0.82
0.82
0.81
0.711
0.711
0.711
0.56
0.33
0.333
0.53
0.51
0:750
0.230
0.750
0.730
0.730
Miitaak------tttet (SoT1 Encodor, prame)
15.00
51.32
67.0
17.15
01441
031
0.36
0.85
0.308
0.540
0.340
0.10
01:
0:57
0.85
0.84
0.54
0.735
0.735
0.704
RL-NN No. 30.27
41.95
06.41
50.1 57.8
0.359
05:
0.87
0:85
0.85
0.86
0.704
0.766
0.700
0,780
0.799
0.11
0,40
0.00
U.53
U.54
0.51
0.50
0.47
0.45
6.147
0.310
0.310
0.047
0.147
0.110
0.147
0.209
11186
all-Minil M+L (Burliie Eacoder, parmm))
16.00
9309
47.51
9099
0117
05:
0.40
0.55
0.53
0.51
0.56
0.273
0.271
0.31
0.18
0.58
0153
0.51
11500
0.47
0.46
0:44
0.300
0.205
0.307
01200
NL 26.35
45.12
54.28
63.75
75.54
0.335
0.51
0.278
0.277
0.31
0.76
0.96
0.63
0.57
0.40
0.155
41135
-1.135
48.13
0.36
0.64
0.50
0.52
-8,00
-8010
.0.19
JU0ID
-0,01
PRoorBRInGI (Pagposed
- FL 52.33 79.51 87.06
91.49
95.08
0.650
03:
0.76
0.71
0.68
0.64
0.58
0.123
0.122
0.121
0.65
22.7M 218M perams)
0.67
0.57
0.49
-0.35
-0.85
-0.85
-0.13
-8.13
M:
0.1
0.50
0.53
-6.09
-6.00
.0.01
40012
NL 51.23 76.77 M6.18
91.50
94.1
00635
0.8
0.A5
indicates that PROOFBRIDGE more frequently retrieves the correct cross-modal counterpart among the highest-ranked results. For the NL and FL embeddings by PROor the median (M) cosine similarity of retrieved cross-modal instances averages 0.64 across top-K (K = 1, 5, 10, 20, 50) in both directions, showing that select cross modal theorem+proof pairs are tightly clustered. In con- trast, non-retrieved instances are much farther apart, averaging - -0.01. Compared to the Baseline, retrieved-pair similarities increase by 23%, while non-retrieved similarities decrease by 104%.
PROOFBRIDGE outperforms the SoTA Encoders in recall and MRR, with a much higher mMG despite being 32x smaller, showing a clearer separation between retrieved and non-retrieved items. For NL. -B--taal-----Istttttt
attains an m.MG of 0.10, while Sereen--mbedding--. -8B reaches 0.29. We believe these low values arise because: first, these QA-oriented encoders capture coarse domain-level signals rather than fine-grained mathematical semantics, so most mathematical texts cluster together; second, as plain-text, non-DAG-award encoders, they rely superficial lexical cues (keywords), but in Lean many proofs share the same tactics, making keyword overlap non- discriminative. In contrast, PROOFBRIDGE leverages the DAG to distinguish proofs, achieving an mMG of 0.65. Overall, encoding Lean proofs via linearized DAG traversals and contrastive align- ment with DAG-aware FL encoder yield effective joint embedding space, where equivalent NL-FL pairs cluster tightly and inequivalent ones remain well separated. This enables reliable re- trieval of the most relevant FL demonstrations to condition the LLM during nuto-formalization.
Proof Formalaomaiiz Table reporrs the proof auto-formalization performance of 13 SoTA LLM-based tools. Theorem auto-formalization LLMS achieve 0% TC and SC across all pass k. These models are designed to formalize theorem statements only. leaving proofs as sorry. They lack knowledge of proof DAGs and tacties, making them unsuitable for end-to-end proof auto- fonngauundationn models, S.emini-2.5-Flash--
formalization. Among foundation TC at pass@32. which increase to 4. 10% SC, 18. 18.44% TC for Flash and 8.61% SC, 31.56% TC for Pro. GPT-5-mini attains 9.02% TC and 34.84% SC at pass @ 32. They struggle with the strict syntax and semantics of specialized FLs like Lean, which are underrepresented in their training data. The SolAA Two-Step achieves 43.44% SC and 59.43% TC, but it is prone to cascading emrors: an incorrect FL theorem from the first model causes the second to produce a semantically incorrect theorem+proof pair. Among the SoTA AFPS LLMs, Simina-Prover-721 achieves the strongest zero- shot performance at pass @ 32, with 46.31% % SC and 79.51% TC. We build PROOF a smaller variant, Kimina-Proo Pwwaae-roooo-----eeeee modal retrieval and using them for eetrieval-augmeene
achieves 2.87% SC and 21.31 %
on top of by retrieving five relevant FL proofs via NL/FL cross-
SFT and inference, along with iterative proof repair. PROOF BRIDGE surpasses the zero-shot performance of Kimina-Prover--ee
by +22.54% SC and 120.499%.0 TC, and its random few-shot performance by +31.14% SC and +1.64% TC.
In Figure 3 we present the pass @ 32 performance across mathematical domains. Following the taxonomy by Zheng et al. (2022), the benchmark includes 6 inductiion/sequence (2.46%), 69 number- theory (28.28%). 90 algebra (36.89%) and 79 contest problems (32.38%) sourced from AIME, AMC, and IMO. GROOFBRIDGE performs best on number theory, achieving over 85% SC, while contest problems remain the most challenging, reaching only about 35% SC.
9

---

Published as a conference paper at ICLR 2026
Table 2: Proof aoto-Formalizztioon Performance. Comparison of LLM- tools on Semantic Correctness (SC) and Type Correctness (TC) across pass k metrics (k E 2, 4, 8, 16, 32))
Setting
LLMi
Semantic Correctuess (SC) (S)
Type Currectaos (5B)
p
pase214
p poss
pa
puser
yu 0:33
13.03
22.54
15.25
40.15
56.15
75:00
Pancc-Dieill-- 73B
18.85
23.77
37. 10
63.52
75.82
25,00
43.03
09.25
79.51
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
Hesal-Toncittrr
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0.00
0107
1100
0.00
010
1.35
0.5
4.5T
9.00
15.5%
"TT.11"
Camini-2 2.S.
Solt Ronks
Genini 2.5
1.23
1.23
3.28
6.9
8.61
18.35
23.77
31.56
frandom
GPU-mmiti
1.23
4.51
7.35
9.00
2008
29.25
34.84
few sho0
DecpSock, Prover-V
5.61
11:07
12.30
14.34
19.67
24.18
35.66
model Leun
6.56
5.30
11:48
13:11
15.00
23.36
23.59
33.61
39.34
Prover SFT
5,33
7.38
12:70
16.39
17.21
25.41
31.56
42.21
Leataelll Prover.V2
9:43
10:06
15.16
18:03
27.87
37.30
41.39
50.4
Frover
12.30
17.33
6066
74.18
V1.35
Kimma
Proves-738 73B
13.95
37.30
27.52
Solt Tools
Kimina Prover R1.1
6:15
12.70
18:35
28.25
52.7%
43.39
53.08
70,06
56.30
89.75
(eet based sotieval
Kinina Dieil--Deii--31 Kinina Pin
13.50
21:72
34.10
36.07
50.92
71.90
96.07
fre-shon
12.29
14.34
24.59
29.51
31.70
44.26
31.15
45.06
64.58
75,62
56.78
68.93
SoTA Tep-Sup
Taanci-- Kininu- Pesiin--------illl-- &B
14.75
19.36
27.05
33.20
38.52
63.46
30.33
32.79
43.03
08.36
54.10
59.45
PRous BRIDGa (SFI only
6,97
13:52
19:26
24.18
29.92
34.84
27.87
45.50
00.66
66.39
72.13
78,69
Our Tool
PRioee Buuoca (Resteral angen. SPT)
13:31
20.90
22.02
35.45
47.04
55.13
29.90
36.11
00:25
71.31
55.20
89.75
PRoiee BRious (Renstral-angert. SPT + Ropaii
16.19
25.41
29.51
37.70
51.41
62.70
31.79
47.15
64.75
78.69
90.16
95.49
5.6 ABLATION STUDIES
100
Domann--wBee Tist Itatannes
To assess the effect of in-context examples, Table ports zero-shot, random few-shot, and text-based retrieval few-shot performance for three Kimina-Prover variants (72B, Distill-8B, and RL.-1.7B). From the pass@33 results, Kimina-Prover--LL1111
80
60
40
achieves 40.16% SC and 75.00% TC in the zero-shot setting, When random examples are added, SC drops to 31.56% while TC rises to 93.85%, with similar trends across variants. This indicates that random examples improve TC (syntax) but hurt SC by causing the model to hallucinate semantically misaligned proofs. With text-based retrieval via Owen3-Embeddinng 8B, SC rises to 32.38% but TC declines, likely because QA-based retrieval favors proofs with similar tactics, reducing tactic diversity. This highlights the need for retrieving semantically relevant examples via a DAG-aware encoder, as in BRIDGB.
20
8
Contest Induction/ Algebr
Number
Problem Sequence
Theory
Both type- and pemantiaall-corree (5C)
Type-cureet only (TC- SC)
Thols left - right. (1oss0e332 performance))
A. Cominii2.5-PPer frusdom feusskot)
DeppSank Prowu-- 1.RR. (rendom Jeasshat) based D. Phone Duman (Redr-asgen. SET Repai)
Figure 3: Category- Results. Proof auto-formalizztion performance across mathematical domains.
To quantify the contribution of each component of PROOF- BRIDGE, we perform an ablation over three variants. PROOFBRIDGE (SFT), fine-tuned on la- beled NL.FFL pairs and evaluated in the few-shot setting with semantically relevant examples via joint-embedding model, improves SC by +2.06% but reduces TC by -11.06% relative to Kimina- Prover-RL-I.7B (text-based retrieval few-shot). Next, in PROOFBRIDGE (Retrieval-augmeente a SFT), we fine-tune the LLM with semantically relevant FL proofs included in the input, achiev- ing 2..2555% SC. PROOFBRIDGE (Retrieval-augmentee SFT + Repair), adding iterative proof repair, yields the best results: +29.92% SC and +5.74% TC over the same baseline. Relative to Kimina-Prove Prover-RL-1.777 (random few-shot), the improvements are +31.14% SC and +1.64% TC.
CONCLUSION
We present PROOFBRIDGE, a unified framework for NL-to-Lean proof nutolformalization that translates both theorems and proofs end-to-end. At its core is a joint embedding model of NL and FL that encodes Lean proof DAGs, capturing tactic sequences and dependency structures. It enables highly effective cross-modal retrieval of semantically relevant FL proofs. These retrieved proofs act as demonstrations, guiding retrieval-augmentt guided repair loop further refines generated proofs by combining Lean type-checking with semantic equivalence checking to ensure correctness. Evaluated on MINIFFF-TEST PROOFBRIDGE sig- nificantly outperforms state-of-the-ar LLMs in both semantic correctness (by bi-directional equiva- lence proving) and type correctness, demonstrating that integrating structured embeddings, retrieval guidance, and verifier feedback leads to more reliable proof nuto-foomalization.
fine-tuning of an LLM. An iterative verifier-
10

---

Published as a conference paper at ICLR 2026
REFERENCES
Kevin Buzzard. Lean 3 Material for Kevin Buzzard's 2021 TCC Course on Formalis-
ing Mathematics. Imperial College London, 2022. URL https: htpp:://githbt tht............. com/
mathemat ics
Accessed: Jan, 2026.
Gheorghe Comanici, Eric Bieber, Mike Schackermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, al. Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities. arXiv preprint wxxiv2557.002611 2025.
Shibaranjani Dasgupta, Chandan Maity, Somdip Mukherjee, Rohan Singh, Diptendu Dutta, and Debasish Jana. HITgram: A Platform for Experimenting with n-Gram Language Models. In International Conference Applied Algorithms, pp. 92-104. Springer, 2025.
Google Deepmind. AI Achieves Silver-Medal Standard Solving International Mathemati- cal Olympiad Problems, 2024. URL wwwvooolssnee probl ems at sellver-medal level/ Accessed: Jan, 2026.
google/ /is.veer/bbbb//////////oo/
Matthew DeLorenzo, Kevin Tieu, Prithwish Jana, Piyush Jha, Dileep Kalathil, Vijay Ganesh, and Jeyavijayan Rajendran. Dbstractions-o--Thoughh Intermediate Representations for LLM Rea- soning in Hardware Design. arXiv preprint arXiv:2505. /5873, 2025.
Kefan Dong and Tengyu Ma. STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving. In 42nd International Conference on Machine Learning (ICML). PMLR, 2025.
Guoxiong Gao, Haocheng Ju, Jiedong Jiang. Zihan Qin, and Bin Dong. Semantic Search En- gine for Mathlib4. In Findings of the ACL: Empirical Methods in Natural Language Processing (EMNLP), pp. 8001-8013. Association for Computational Linguistics, 2024.
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A Natural Language Annotated Lean 4 Dataset. In 13th International Conference on Learning Representations (ICLR). OpenReview.net, 2025.
Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward Ayers, and Stanislas Polu. Proof Artifact Co-Training for Theorem Proving with Language Models. In 10th International Conference Learrnnng Representations (ICLR). OpenReview.net, 2022.
John Harrison. HOL Light: An Overview. In International Conference on Theorem Proving in Higher Order Logics, pp. 60-66. Springer, 2009.
Debasish Jana. C++ and
Programming Paradigm. PHI Learning Pvt. Ltd., 2014.
Debasish Jana and Debasis Bandyopadhyay. Efficient Management of Security and Privacy Issues in Mobile Cloud Environment. 2013 Annual IEEE India Conference (INDICON). IEEE, 2013.
Debasish Jana and Pinakpani Pal. ESSENCE Kernel in Overcoming Challenges of Agile Software Development. In 2020 IEEE 17th India Council International Conference (INDICON). IEEE, 2020.
Debasish Jana, Pinakpani Pal, and Pawan Kumar. Real-Time Agile Software Management for Edge and Fog Computing Based Smart City Infrastructure. In International Conference on Computing and Communication Networks, pp. 113-121. Springer, 2025.
Prithwish Jana. NeuroSymbolic LLM for Mathematical Reasoning and Software Engineering. In 33rd International Joint Conference on Artificial Intelligence (IJCAI), pp. 8492-8493, 2024.
Prithwish Jana, Piyush Jha, Haoyang Ju, Gautham Kishore, Aryan Mahajan, and Vijay Ganesh, Co- Tran: An LLM-based Code Translator using Reinforcement Learning with Feedback from Com- piler and Symbolic Execution. In 27th European Conference on Artificial Intelligence (ECAT), pp. 4011 4018. IOS Press, 2024.
Piyush Jha, Prithwish Jana, Pranavkrishna Suresh, Arnav Arora, and Vijay Ganesh. RLSF: Fine- tuning LLMs via Symbolic Feedback. In 28th European Conference on Artificial Intelligence (ECAI), pp. 1687-1694. IOS Press, 2025.
11

---

Published as a conference paper at ICLR 2026
Albert Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language Models of ISAbelle Proofs. In 6th Conference on Artificial Intelligence and Theorem Proving (AITP), pp. 378-392, 2021.
Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. In 11th International Conference on Learning Representations (ICLR). OpenReview.net, 2023.
Albert Q Jiang, Wenda Li. and Mateja Jamnik. Multi-Language Diversity Benefits Autoformal- ization. In 38th Annual Conference on Neural Information Processing Systems (NeurlPS), pp- 33600-83626.. Curran Associates, Inc., 2024.
Leanprover. leanprover-communittttat
Simple REPL for Lean 4, 2025. github. com/ www.://eeaanooeeeooooooooeooeeee tt repl Accessed: Jan, 2026.
URL https://
Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin,
Roman Soletskyi, Shengyi Costa Huang, Kashif Rasul, Longhui Yu, Albert Jiang, Ziju Shen, Zihan Qin, Bin Dong, Li Zhou, Yann Fleureau, Guillaume Lample, and Stanislas Polu. huggingface... Stw.giinnfacccccAAT---A 2026.
NuminaMath, 2024. URL https:// Hugging Face Dataset, Accessed: Jan,
haMath-1.5
Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang. Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, al. Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving. In 2nd Conference on Language Modeling (COLM), 2025.
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval- Approach. In 13th International Conference on Learning Representations (ICIR), 2025.
Janniao Lu, Yingjia Wan, Zhengying Liu, Yinya Huang, Jing Xiong, Chengwu Liu, Jianhao Shen, Hui Jin, Jipeng Zhang, Haiming Wang, et al. Process-driven Autoformalization in Lean 4. arXiv preprint arXiv:2446.00/ 0/940, 2024.
Patrick Massot, leanblueprint: plasTeX Plugin to Build Formalization Blueprints, 2020. URL Accessed: Jan, 2026.
https: /ttp:/:///tttttttt wwt.e////aataaaaaaeaeeee
Norman Megill and David A Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu. com, 2019.
Leonardo de Moura and Sebastian Ullrich. The Lean Theorem Prover and Programming Lan- guage. In Automated Deduction-CAle CCDE 28: 28th International Conference on Automated Deduc- tion, Virtual Event, July 12-15, 2021, Proceedings 28, pp. 625-635. Springer, 2021.
Tobias Nipkow, Markus Wenzel, and Lawrence Paulson. Isabelle/HOL: Proof Assistant for Higher-order Logic. Springer, 2002.
MutinaMath. test Hugging Face Dataset, 2025. U URL:httpp::/uogginfaacccco
Cataaetts/AT-MM//iiiffft test Accessed: Jan, 2026.
OpenAI. Introducing GPT-5, 2025. Accessed: Jan, 2026.
URL https://openai.comm
Introducing 5/
Lawrence C Paulsson and Jasmin C Blanchette. Three Years of Experience with Sledgehammer, Practical Link Between Automatic and Interactive Theorem Provers. 8th International Work- shop on the Implementation of Logics (IWIL), volume of EPiC Series in Computing. 2010.
Gabriel Poesia and Noah D Goodman. Peano: Learning Formal Mathematical Reasoning. Philo- sophical Transactions of the Royal Society A, 38 (22112))) 2023.
Auguste Poiroux, Gail Weiss, Viktor Kunčak, and Antoine Bosselut. Reliable Evaluation and Bench- marks for Statement Autoformalizatoon. In 2025 Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 1 17958-17988 ACL, 2025.
12

---

Published as a conference paper at ICLR 2026
Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv preprint arXiv:2009.033: 03393, 2020.
Nils Reimers and Iryna Gurevych. Sentence-BERT: Sentence Embeddings using Siamese BERT- Networks. In 2019 Conference on Empirical Methods in Natural Language Processing (EMNLP).
ACL, 2019.
ZZ Ren. Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang. et al. Deepseek-Provers Advancing Formal Mathe- matical Reasoning via Reinforcement Learning for Subgoal Decomposition. arXiv preprint arXiv:2504.2180) 2025.
Ziju Shen, Naohao Huang, Fanyi Yang, Yutong Wang, Guoxiong Gao, Tianyi Xu, Jiedong Jiang, Wanyi He, Pu Yang, Mengzhou Sun, al. REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning, arXiv preprint arXiv:2505.2061 2025.
Matthieu Sozeau, Maerre-Marie Pédrot, et al. The Rocq Prover, 2025.
URL https:
rroe-prover.oog/ Accessed: Jan, 2026.
Terence Tao. A Maclaurin Type Inequality. arXiv preprint arXiv:2310.053388, 2023.
Amitayush Thakur, George Tsoukalas, Yeming Wen, Jimmy Xin, and Swarat Chaudhuri. An In- Context Learning Agent for Formal Theorem-Proving. In 1st Conference on Language Modeling (COLM), 2024.
Shubham Ugare, Tarun Suresh, Hangoo Kang, Sasa Misailovic, and Gagandeep Singh. SynCode: LLM Generation with Grammar Augmentation. arXiv preprint arXiv:2403.01632, 2024.
Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, al. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning, arXiv preprint arXiv:2504.11333 2025.
Liang Wang, Nan Yang, Xiaolong Huang, Linjun Yang, Rangan Majumder, and Furu Wei. Improv- ing Text Embeddings with Large Language Models. In 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Pupers), pp. 11897-11916 ACL, 2024a.
Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. Theorem- Llama: Transforming purrooe LLMs into Lean4 Experts. In Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 11933-11974, 2024b.
Yuhuai WU, Albert Q Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with Large Language Models. 36th Annual Conference on Neural Information Processing Systems (NeurIPS). 35:32353-32368, 2022.
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, and Xing Hu. StemainnFormalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge- Reasoonin Fusion. In 40th Annual AAAI Conference on Artificial Intelligence (AAAI), 2026.
Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large- Scale Synthetic Data. arXiv preprini arXiv:2405. 14333, 2024a.
Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, al. Peepeeck-Prover-vl. 5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte- Tree Search. arXiv preprint 2408 08152, 2024b.
Kaiyu Yang. miniF2FFlean4. GitHub repository, 2025. URL https: com/ yangkyl1/minir22 1ttp://///miii2-eeaaaaaa
Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem Proving with Retreeval-Augmented Language Models. In 37th Annual Conference on Neural Information Processing Systems (NeurIPS). Curran Associates, Inc., 2023.
13

---

Published as a conference paper at ICLR 2026
Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean Workbook: A Large-scale Lean Problem Set Formalized from Natural Language Math Problems. In 38th Annual Conference Neural Information Processing Systems (NeurIPS), pp. 105848-105863. Curran Associates, Inc., 2024.
Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, and Kun Gai. Leanabell-Prove Posttraining Scaling Formal Reasoning. arXiv preprint arXiv:2504.06122, 2025a.
Yanzhao Zhang, Mingxin Li, Dingkun Long, Xin Zhang, Huan Lin, Baosong Yang. Pengjun Xie, An Yang, Dayiheng Liu, Junyang Lin, al. Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models. arXiv preprint arXiv:2506.0552 2025b.
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. MiniF2F: A Cross-System Benchmark for Formal Olympiad-level Mathematics. In 10th International Conference on Learning Representa- fions (ICLR). OpenReview.net, 2022.
Yuhao Zhou. Betrieval-Augmentn TLAPS Proof Generation with Large Language Models. arXiv preprint arXiv:2501 00000003, 2025.
14

---

Published as a conference paper at ICLR 2026
A APPENDIX
A.1 THE USE OF LARGE LANGUAGE. MODELS (LLMS)
LLMs did not play a significant role in either the research idcation or the writing of this paper. Their use was limited to correcting minor grammatical issues and typographical errors.
A.2 REPRODUCIBILITY AND DATASETS
All implementations in this work, including dataset construction, model training, cross-modal re- trieval. inference, and evaluation, use Python 3.12.10 and Lean v4.15.0. Experiments were con- ducted high-performance Almal Linux 9.5 (Teal Serval) cluster with single Intel Xeon Platinum 8480+ CPU (32 cores, 2.0-4.0 GHz), 251 GiB of RAM, and one NVIDIA H100 GPU. Our full code- base, including scripts for dataset generation, model fine-tuning, and inference across both GPU- and API-based setups, is available at tihttps: psttpps://// /
com Prri/rritte tewitsh.... wetwwshae www.wiwwhaaaaas...a fBridge The repository well documented and includes instructions for creating a Python virtual environ- ment, along with comprehensive README detailing library dependencies, dataset formats, and step-by-step instructions to replicate the entire data pipeline and experimental workflow.
Through our repository, we release
and MINTF2F-TEST-PE follow- ing the respective licenses (Apache License 2.0 or MIT License) of their source datasets. Note that our AUMINAMATH-LEANNE
dataset is carefully refined and extended from NuminaMath- LEAN (Wang et al., 2025), while MINIF2F-TEST-PF is curated by combining two versions of miniF2F-test (Zheng et al. 2022) from(NuminaMath (2025) and Yang (005)). The original datasets were built by collecting problems from web sources, forums, and online documents, including worldwide competitions such as AMC, AIME, and IMO, well public K-12 exam papers. For each problem, the corresponding Lean theorem and proof were produced either by human annota- tors via L..M-based formalzer....... Formalizing large-scale proofs often requires agile methodology (Jana & Pal, 2020) Jana et al.] 2025). dividing proofs into small, manageable lemmas that can be handled by different human annotators. Many large-scale Lean projects now use tools such as leanb luepriiin int (Massot (020), which serve as planning and coordination resources, en- abling contributors to track progress, visualize dependencies, and identify remaining formalization tasks. Because the pipeline aggregates material from problem authors, human formalizers, LLM- based auto auto-formalizers, textbooks, competition archives, and exams, it is important to ensure proper privacy, licensing, and copyright compliance (Jana & Bandyopadhyay 2013).
A.3 TRAINING AND INFERENCE HYPERPARAMETERS
NL/FL Cross-Modal Retrieval. We train two dense encoders to embed NL and FL theorem+proof pairs into a shared semantic space. The NL encoder is initialized from all-Mini LL-LLL----ML---------- -6-v2 (Reimers Gurevych| 2019), while the FL encoder builds on Lean- Dojo's Yang et al., 2023) ByT5-based proof-state encoder, extended to process linearized traversal of the proof DAG. Each encoder is equipped with a projection head that maps representations into a shared embedding space of dimension d = 512, with a dropout rate of 0.1. During fine-tuning, update only the top layers of each encoder to retain their pretrained linguistic and structural priors. Specifically, we train the last 3 layers of the NL encoder and the last layers of the FL encoder. We set the maximum token length to 512 for both NL and FL sequences. The model is optimized using our symmetric contrastive objective (Equation]] D with temperature with learning rate of 1 x 10 10-5, 55, weight decay of 0.01, and batch size of 32. Training is run for 10 epochs with gradient accumulation steps set 4. We also enable gradient checkpointing to reduce memory usage during fine-tuning.
0.07, trained using AdamW
Proof Auto-Formalization PROOFBRIDGE builds on 2025), which we further fine-tune for NL-FL translation using paired data (MxL Mrl) from NUMINAMATIILLENN PF. During both SFT and inference, our NL/FL cross-modal retrieval model gets the top-5 most relevant FL proofs from D. which are provided as in-context demonstrations to guide Lean proof synthesis. We use the HuggingFace Trainer for supervised fine-tuning with the following settings: a per-device batch size of 8 and BF16 training enabled. Training is run for 5 epochs with a learning rate of x 10 6 cosine decay scheduling, and a warmup ratio of 0.05. For all SoTA baselines in Table 2 we compute pass @K k using stochastic decoding. Specifically, we
(Wang et al,
15

---

Published as a conference paper at ICLR 2026
LLM inference with temperature of 0.6 and top-p sampling of 0.95, ensuring sufficient diversity across generated candidates.
A.4 SEMANTIC EQUIVALENCE OF LEAN THEOREMS
Lean (Moura & UlIrich 2021) a functional programming language in which functions are first- class values, treated like any other data type (Jana 2014). The task of auto-formalization is to convert a mathematical theorem and proof from natural language (NL.) into a formal language (FL.,, such as Lean. When evaluating the performance of such systems, we propose two criteria for evaluation: type correctness and semantic correctness. Type correctness, which requires that the generated Lean proof is accepted by the Lean type-checker, is straightforward evaluation metric in the field. In contrast, semantic correctness, which ensures the FL theorem faithfully represents the meaning of the original NL theorem, presents a far greater challenge. To the best of our knowledge, such semantic equivalence has not been systematically evaluated in prior work. This section introduces novel methodology address this gap.
verify and serves the standard
While directly measuring the semantic aligmment between NI. theorem and a Lean theorem is an unsolved challenge, showing the logical equivalence of two Lean theorems is tractable task. Our training dataset, NUMINAMATH-LEAN
contains pairs of (TNL.TFL. where most of the TEL were manually created by experts at Numina. We treat these high-quality TiL theorems as gold- standard references, assuming they are faithful translations of their TNL counterparts. This allows us to reduce the intractable problem of verifying a model's 's generated theorem TeL against the original TNL. to the more tractable task of checking for logical equivalence between TEL and the gold-standard reference Tr. which can be checked in Lean itself.
To be more specific, enforce this semantic equivalence check by proving the logical biconditional TEL <> TFL in Lean. Theorems like TrL and TiL are of type Prop in Lean. The following theorem from Mathlib states that for any two propositions, logical biconditional between two propositions itself logically equivalent to their propositional equality:
theorem propext__ iffla b. Prop) = b + (a 4> b)
The task thus converts proving the equality TF. TA. within Lean. This requires clarifying the specific notion of equality being used, as Lean distinguishes between three primary types: syntactic, definitional, and propositional (Buzzard 2022). Syntactic equality is the strictest form of equality in Lean, as it only admits expressions that are structurally identical according to their Abstract Syntax Trees, without any computation or reduction. Definitional equality a more relaxed form of equality than syntactic equality, where two expressions are considered equal if they compute or reduce to the same normal form. Propositional equality is the weakest form of equality, and also the standard notion of equality used in mathematical theorems. Two terms a, b are propositionally equal in Lean if we can construct a proof term for the proposition a b.
For our evaluation, we seek to measure how closely a TeL matches the TFL. The strictest criterion, syntactic equality, is too restrictive given the current state-of-the-art, it would fail valid theorems with trivial notational differences. Conversely, full propositional equality can be too permissive; a proof of equivalence can be arbitrarily complex, making difficult automate and decide.
Therefore, we adopt a pragmatic compromise: we check for definitional equality supplemented by a form of bounded propositional equality. This means we primarily check if Trr and TFL reduce to the same normal form, but we also permit some propositional equality, provided they can be proven using a collection of tactics so that their proof complexity is bounded.
We then leverage Gemini 2.5 Pro as an automated equivalence checker. The model is prompted to synthesize a proof for the biconditional theorem (TFL ++ TFL), with instructions limiting it to specific subset of available tactics. This restricted set includes three powerful automated tacties, rfl, simp, and ring, each is designed to discharge specific class goals: rfl for definitional equality, s simp for simplification, and ring for polynomial identities.
As definitional equality is our primary target, the equivalence checker first attempts to solve the goal with the f1 tactie. This single tactic should suffice for the majority of cases. If r11 fails, the
16

---

intro Published as a conference paper at ICLR 2026
checker then tries simp. This tactic performs additional simplifications by rewriting the goal using theorems from Mathlib that are tagged for its use. Critically, we use simp without any arguments. Providing explicit arguments would require demanding search for the correct lemmas and could introduce unbounded complexity, violating our goal of a bounded proof search. Furthermore, the need for mi with arguments could imply that the required rewrite is non-trivial, since the default simplification set contains most of the trivial facts Since our goal is to ensure close correspon- dence between TF. and TA. proof requiring such targeted rewrite indicates a semantic distance that we classify as mismatch. The ring tactic is a valuable complement to the previous tactics as it specializes in proving polynomial equalities. The ri ring tactic operates by reducing arithmetic expressions to a canonical normal form. This allows it to prove the equivalence expressions that algebraically identical but not definitionally so, such as x x22 and x, which rfl and default s simp would otherwise fail to solve.
The three tactics discussed above cover most of the direct equivalences we aim to check. The maining tactics in our instruction set are designed for a more nuanced case: proving the biconditional when two theorems differ only in their use of auxiliary variables. We observed that human experts and language models may make different but equally valid decisions on whether to introduce an auxiliary variable. We therefore classify such theorems as equivalent. For example, consider the following:
def Propl :- (V (b h R), (0 b
A
0
h 0
< v) + (V 1 /
3
(6
h)) + (b 30) (h 13 21
V 65)
def Prop2 := (V {B h : R2, (B 30)
7 (h 6.5)
+ 11 / 31 * h 65)
example : Propl + Prop2 := by
constructor
simp
ring
simp
intros
nlinarith
The main difference between the two propositions Propl and Prop2 the presence of the auxiliary variable in one. To prove that such theorems are equivalent, one must typically prove the bicon- ditional by separately proving the implications of both direction. This requires step-by-step proof construction, and the tactics above are included in our instruction set.
Finally, we note that the LLM judge's role is only to synthesize a biconditional proof under the bounded tactic set described above; the produced proof is then fully type-checked by the Lean kernel, so the SC decision ultimately depends on Lean's verifier (making the metric conservative rather than prone to false positives).
Comparison with Existing Semantic Correctness Metries. Prior work has proposed similar se- mantic correctness metrics, including BEq (Liu et al. 2025 Wu et al., 2026) and its extensions BEq+ (Poiroux et al. 2025). While the general idea behind our SC metric and BEq is similar, both aiming establish bidirectional equivalence in Lean, the sets of allowed tactics differ. Because the notion of equivalence depends on the permitted tactics, these differences lead to meaningful distinc- tions between SC and BEq. BEq+ is reference-based metric inspired by BBq and uses set of tactics comparable to SC. However, BEq+ is deterministic and CPU-efficient, while SC relies on an LLM-bbased proof synthesizer. This creates a trade-off: the LLM can capture equivalences beyond the reach of the deterministic procedure, whereas BEq+ provides reproducible evaluation.
Consider Prop1 and Prop2 above as an example. Prop1 (gold-standard FL theorem from min Test-PF) explicitly introduces an auxiliary variable v to denote volume, whereas Prop2 (produced by Kimina-Pruss Pro----oovee--------
omits the auxiliary variable and substitutes the corresponding formula directly. The tactic set allowed by BEq is not expressive enough to establish equivalence in such cases, so these theorems would not be recognized as equivalent under BEq. Our SC metric, by contrast, was specifically designed to handle such variations, reflecting the fact that human experts may also differ in whether they introduce auxiliary variables. By explicitly handling these variations
It is important to note that the default simp set intentionally excludes lemmas like associativity and com- mutativity, as they can cause the simplifier to loop indefinitely. However, since these lemmas primarily concem algehraic expressions, they can be handled by the ri ng tactic.
17

---

Published as a conference paper at ICLR 2026
and using LLM- -eaeeratd bidirectional proofs that type-checked, SC provides evaluation that is both more lenient and faithful in assessing the performance of auto-formalization models.
A.5 ILLUSTRATIVE EXAMPLE
We present an example of an NL theorem+proof pair from MINIF2F-TEST-PF and compare the pass@l output of proof fortalziaaiinnion generated by Jimina-Prover-Ree retrieval few-shot setting with that produced by PROOFBRIDGE (using Retrieval-augment Repair). We first show the retrievals of semantically relevant FL theorem+proof pairs from D, followed by the passš output proof cotto-fommliiation generated by PROOFBRIDGE, In this example, the output by Mimina-Proove-RL.. RL-1.7B is type-correct (TC) but not semantically correct (SC), i.e., it is not bi-directionally equivalent to the gold-standard Lean proof. In contrast, the output by PROOFBRIDGE both TC and SC.
in the text-based SFT
Input NL theorem+proof pair (MINIF2F-TEST-PM)
<informal, ttheore>>
point (x. y) the coordinate plane with both coordinates negative is distance of 6 units from the æ-axis. is distance 15 units from the point (8, 3). a distance v the origin. What n??
Show that is 52.
</informal.t theorrem
<informal -proff>
We know that y -6 from the given information. By the distance formula, have the equation
v 8)
+ (-6 6- 3)2 15. Solving, we have
V(x 8)2 + (-6 3)2
16x 64 225
x² - 16x 80 0
(x 20)
Thus, +44 = 0 or x 20 = 0, so
20. r - by the given conditions. Thus, our point
(-4, -6) and is distance of v(-4)² (- </informal -oooorrmllpprof>>>>>
/52 units from the origin. n 52.
Gold-standard Lean theorem (MINIF2F-TEST-PF)
import Mathlib
import Aesop
set_opttion maxReartbeats 3
open Sig0peratozs Real Nat Topology Rat
theoren mothé_algebre 263 ix y. : R) in : NNkeel) (hg : x 0.0.A.. 0) Ohr abs y = 6)
(ha Resl.agrt
2
151
(hs Real.agrt (x 2 2) Real.agrt r) 52 by sorzy
Output Lean proorem+proof pair by Kinina-Prover-RI-- (text-based retrieval few-shot setting)
import Mathlib
/- A point 1x,)) en the coordinate plane with both coordinates negative is distance of unite Erem x x-axis. is distance 15 unite distance (sgrt(a) from the crigin. what is n2 shou that it is 52.-/
peint (8,3), is
theorem algebra_60se 10922
N) thn ((x ") (y "2) = A /1x22 2) Vol 52 by ccases with (x, y, hx, hy, bi, h2, h3) have hy1
th 3 y B, ExxAAySOOR lyl
: by
cases' abs_cases
hy2 hy2
1imarith
llaarith
have h2' 81"2 31"2 2 225 cale
18

---

Published as a conference paper at ICLR 2026
1x "2 13 31 = (V(xx 81"2 31/2)) ? 2. xm by zv (seal.ag_oqit))
positivily
15 :- by IM [H2]
(225
by
rw [hy1] 1 at h2
h2x
144 by nlinarith
have hxl
-4 by
nlinarith [a2x, hx]
have h3' x y (n R1
cale
x'2
(V(x22 222))
(Real.eg__gert) positivity
(/a)
by [h3]
Ri by [Rea). sa_aart) positivity
[ixl, hyl] h3
have hnn : (a : R) 52 :- by alinarith
have hn2 52 by
sract__mod_cme cast hn!.
exact_mod_caatt
Note that, although the Lean theorem generated by Simina-Prover--RL-. is type-correct (TC), differs semantically from the gold-standard theorem. The main difference lies in the quantification of variables. the gold-standard theorem, the variables z, y, n are universally quantified explicit arguments, and all hypotheses are stated as direct assumptions; this asserts that for any triple (z, V. n) satisfying the geometric constraints, versally quantífies but existentially quantifies and within the hypotheses. This more accurately reflects the intended geometric meaning: for a given n satisfying the distance constraints, there exists point (ır, y) realizing those constraints, and consequently are syntactically valid in Lean, they encode slightly different logical statements. This difference pre- vents LLM judge from producing type-checkable proof of bi-directional equivalence between the two theorems. As a result, the Aimina-Prover-RL..
52. In contrast, the Kimina- Prover-oo------ RL-1.7B output uni-
52. Therefore, while both theorems
output is not semantically correct (SC).
Comparison between the gold-standard theorem and Paaiina-Proer-RII---.. output
Gold standard theorem -/ R) (n (NNkes) (he x
theorem mathé_algebra
0)
abs
(hg Real.agrt (ix 8) 2 ty - 3) 2) 151
(hs Real.agrt
by
sorzy
Kimina Provez RL 1.7B output theorem -
theorem 60922 in : N) (hn : a 1) th xxy: c ((x - 81 "2 ( 31"2) - 15 A vix"2 + 272)
52
by
sorry
Below, we present the relevant FI. theorem+proof pairs (demonstrations) from D retrieved by PROOFBRIDGE, along with their relevance scores.
Lean theorem+proof pairs retrieved by PROOFBRIDGE'S NL/FL Cross-Modal Retrieval
###
Relevant Lean proor with relevance score 0.786764 out of 1.0
import Kathlib
/- Find the distance hetween the points (2,2)) 3--1--1)6 -/
theoren algebra_1318 13734 (pl p2 : R x R) (hpi pi (2. 2)1 1892 92 (-1, -10) Real. Real.agrt sgrt == by
Real.agrt ((pl.1 p2.11'2 2 1p1.2 p2.2) [hpl, hp2]
nоrm_лоa ring
rw wgw.o_oggo.fff..ooooooooe. iff iff__a_ooggl ring nomm_nus
<1> norm_num
### Relevant Lean theorem+proof with relevance score 0.768226 out of 1.0
import Matalib open Real
1- Prove that the angle (In degrees) between the vectors $ 12,55) and 113,, 31 i. $439. -/ theorem calculus_
(-3)
lagrt 5 2) sgrt (1-3) + 251 180
π = 45 :- by
19

---

by Published as a conference paper at ICLR 2026
have 12 (-3) +
(agrt
sgrt (1-3) 21)
Real.aqr agrt 2 2. by
have h2 aqrt (12 31 (5
Seet 29 =- by
norm_num [Real, Reallssert_ee_iie
agrt ((-2 it__rt______f____________
R) 2) heel..err
nerm_num
have bd 12 3) 7 R) 29 nozn
h4]
Beal aggt Real. sgrt seal.sgrt 129 om by cale
Real.sqrt 29 Real, sqrt Real.sqrt sqrt 129 58 sm by norm_num)
[4- seaa_.qgt_mmul
RJ) : by norm num. Real .gl.t RR) Real.sqrt (129 RR)
Keal.sgrt (12 : R) 129
zv [Real. (by norm_num)]
Real.sgrt R) (29 1= by
[Real.aqrt_ (by norm_nimm]]
field_simp [h5]
<t> ring_nf <3> norm_num [geal.
[hi]
have h5 arccos Rhallsgqrt 2 Real.pl .p. 4 have h6 Resl.egrt / Real.cos (Real.pi / =- by
/seal.coo_pp_cci__for
<;> ring_nf <t> norm_num
ring re [h6]
arecos [Real.cos (Real-pt / 4)) Real.pí by
apply arccos_cos
gol_s linerith [Resl.pi_pos]
exect 27
[h5]
field simp [Real.pi_pos] linarith [Real.pi_gt_then
### Relevant Lean theorem+proof with relevance score 0.765285 out of 1.0
Import Mbthlib
1- Show that the sum of $/sert 3x + 2x 115 and SNegrt (3x"2 4x - 238 is at least $
\egst/511/3$ 201318 1x R)
real
theorem inequalition atapolllttaa__1111
kesl.sqrt (3 x 2 +
1) keal.sqrt 13 x'2
21 N
Real.agrt 51
aet y :- Real.sgrt 13 x
x
set Real. sqrt
have hy2 : 2 =3 x'2 + x by rw [Real.eq_aqrz]
nlinarith [sq_nonneg (x + 3)
have hz2 : z'2
x'2
+ by
[Real. sq_aar]
nlinarith [eq_noane (x - 2 3)] hy4_pes
(3 x'2
by
nlinarith [sg_nonneg (x . 3 + 1)]
R) by nlinarith [sq_nonneg (x 3 - 2)]
ho4_pcs S (3 x'2
have hil : (Resl.egrt 51 3)
151 / :- by
iReal.aqrt 51 / 3) 2 (Real.agrt 51) 2 / :- by ring
(51 9 zu (Keal.ag_ (by norm_num)
by
<;> ring
have h50
by ulinsrith Isg (y - zl, sg_noaneg (x / 3), sq_nonneg Ix 3) hi1, Reall.arrt_noneer
2 (Real.aqrt 51
seal.
S R) norm_num),
mul mui_aonneg (Reai. 2) aq_nonga x"2 21)1
(3 x v x 1) [Real.egrt_zonnes (3 à x 4
2), nonnogg ly Real. sgrt (13 x*2
11
20

---

linarith Published as a conference paper at ICLR 2026
have h51
2 0 := by positivity by positivity
have (Real.aqs
3)
have h52 8l (Real. 51 31 by
have h15 (y 2) 2 igeal. 51 3) :-
(Real.sert 51
have h17 (y
(Resl.sqrt 51 2.0 by
nlinarith [sg_nonneg (ly
18sa 51 2)1,
ag_ncnneg (ty + z) (Real.sqrt 51 / 31), Real poal.- (show (0
by inarith (51 R)
linarith
### Relevant Lean pheorem+proof with relevance score 0.764932 out of 1.0
import Mathlib
open Real Set open acoped BigOperators
Given that Siggrt (x-3) '2 (y+4) "2] Anget [xx+5) (y-8) 12] 209, prove that the
distance betwean 5(-5,8) and 913, 1. (13)9 -/
theoren algebra_1083
y RF sqet 31"2 4) agrt 51
8) = 20)
sqrt [(-5 31 72 18 1-41172)
sext by
have h1 sgrt (1-5
3)
(-4))
208
norm_num
[hi]
have h2 agrt 208 aqrt 13 :- by
<t> ring_nf <;> norm_num nomm_num
Iw [ReaL. _qq_]_ 22>
IW [h2]
all_goals
### Relevant Lean theorem+proof 5, with relevance score 0.755091 out of 1.0
import Matalib
/- Show that the square rost of 8 1-31 in $38, that $38 is non-negative, and that $38 aquared equals ( squared.
theorem algebra_8223 8272 Rea ((-3)
372 (-3) 2
have hi Real..grt (1 3 R) 2) by seoallssrt_sg__ee___.
norm_nam constructor
exact h1 constructor nora_num
The proof auto-formalization generated by PROOFBRIDGE is follows:
Output Lean theorem+proof pair by PROOFBRIDGE (Retrieval-augmenned SFT Repair)
Kathlib
/- point 18,9) coordi nate plane with both coordinates negat! 1a disttance of
unite from the axis, It is diatance of 15 unita fzom the point (8, 3). It is distance \sgrt(a) from the crigin.
52.-/
theorem algebra_Ssaa 53819 (x y R) Keal.sgre sall
thy y 0) abs y 61 2) 151
22 2
Real.aqrt ix -
Real. 52, by
hyó -6 by
cases _g_or__e__neg_o__aaeee _ee_____________________________ bl with
linarith
linarith
have h3 (x 8)
18 33
225 = by
ix 8) 2 (y
31 (Real. sqrt ((x 8)
1y 3) 213 2 = by
Skeal.sg_agrt positivity
:- by
(h2)
225 :- by
21

---

Published as a conference paper at ICLR 2026
norm_num num
(hy6]
have h4 (x
2 144
ulinarith
h5
by
have h6 1x 81
144 =0 by linarith
12)
by
nlinarith
cases peroomm hT) with
inl 28
left
Linacith
inz 29 ->
right
linarith
cases with
inl h5
have hx20 : x 20 :- by linarith
linarith
inz h5 m>
:
linarith
have h2 x.x x
2- 52
Iw [2x4, 1y6]
have h8 Keal.sgrt [17]
2) seal.sgrt 52 x= by
exact 26
The Lean theorem generated by PROOFBRIDGE and the gold-standard theorem are semantically equivalent. Both correctly capture the intended geometric scenario: the point with negative co- ordinates satisfying the given distance constraints is at a distance of V52 from the origin. Using our set restricted tactics, the LLM judge able to generate a type-checkable proof establishing the bi-directional equivalence between the two theorems. Therefore, the GROOFBRIDGE output is semantically correct (SC).
Comparison between the gold-standard theorem and PROOFBRIDGE'S output
Gold standard theorem R) (n (NResl) (he x C.1 abs theorem mathé_algebra_288
(hg Real.sgrt (ix 8) 2 ty 3) 2)
151
(ha Real.agrt
y Real
by
sorzy
/- ProofBridge output theorem -/
theorem slgebra_53B8 53819 (x y R) (hx : 8) tay 0)
(h1
abs y 61 (h2
keal.sgrt B) 2
2) 151
Real.aqrt ix 2 + y 2) Real .sgtt 52 by sorry
Lean proof of bi-directional equivalence between PROOFBRIDGE'S output theorem and the gold-standard
import Mathi Anallb..nnalll Analysta Speci Funct
import Matalib. AattlibbData.... Data. Sww.eel..BB.... Beale open Bigopezatozs
Topology
No defing the two atatementa as propositions to prove thefr equi va lenoe.
def aaachda__gabrr___ _asrt______ttt_____ae stmt 1= NNReall
(hr y 6)
(b2 Resl.sgrt (ix B) 2 (y 31 2) 15:
(ig kesl.sqrt ix
2) seat.sqrt
2),
der algebra__3880 stmt 2
V
(bx
1 < 0) (h1 abs G)
(h2 : .ggrt (1x 8) 2 (y 31
21 18),
Real.aqit
2) Real.eqrt
Proef bidirectional eguivalence
theorem aeuivalence mathd_a wergggrbbbr___eeeeee stmt al 0ebra__58111 9_ttm == by constructor
Proaf that aathab_lggbbaa__oo stm_ implica algebra__5aa 53381 stmm intro h_
22

---

Published as a conference paper at ICLR 2026
intro hx by hi b2 use h mathh_atmt,
need provide value for "n and proof for Letta define 'n" as che value of "x"2 + y"2",
First, we need to show 'x"2 y"2" non negative to create an 'WReeal h_nonneg
y
by positivity 2, haaonneg)
let n KNReal :- (x 222 2 hypothesis
now holds by definition of 'n'.
have h3 Real.sgrt (x
2) seal.squt 1= by
stmp [n, NNReal-coe_nk cco__n]]
The hypochesia "ho" is equivalent to 'hx " and Myy, < :- (bx, hy)
have ho : x apply
Now
stacement.
have n_eg_52 : a 52 :- hunathd_stmt x ho h1 h2 h3 our goal
aget 52". No can rewrite 'h3" using 52 to achieve the goal. rwa [n_eg_32] at h3
sest
y
Proof that 53818 intro b_olgebra_attm
implies mathd 208_
intro y.y n ho h1 h2 h3 hypotheses
second statement are avaiiable.
have h_sert_val Real.agrt (x 22-2 +
21 Real.sqrt 52 :-
ILalgebra_stan
y h0.1eft rigtight
le given W:31; "Real.egrt ix 2 2) Reai.agrt a² By transitivity, Nesl.agrt seal.sgrt 52".
aqrt_n__ _______arr___a Real.agrt IW [t h3, h_sqrt_val]
Real agro 52
injective on non-negative numbers, muot aqual 152% Ne get the equality 'R first. have __ ta
since 'Reai.sgrt"
52 :-
I8eal. meal.sgrt_ing n.property (by norm_num)) .p sqrt_n_eg__q=t_52 Then me lift this aquality to "WReol
WNReal.eg n_val_ee_M2
23


Reviews:
[{"review_id": "YuBZZ0CdrY", "reviewer": "Reviewer_gM22", "summary": "This work presents a framework (ProofBridge) for end-to-end translation of entire natural language (NL) theorem-proof pairs into a formal language (Lean). ProofBridge has 3 modules:  (1) a joint embedding model trained via contrastive learning to align NL and FL representations in a shared semantic space, (2) retrieval-augmented fine-tuned LLM conditioned on retrieved FL examples, and (3) iterative proof repair using Lean's type checker and LLM-based semantic equivalence verification. This work also includes the curation of two new datasets: NUMINAMATH-LEAN-PF (38.9k NL-FL pairs) for training and MINIF2F-TEST-PF for evaluation.", "questions": "1. What quality control measures were applied to the Gemini-generated NL proofs?\n2. Breakdown of errors by type (syntax errors, wrong theorem, wrong proof strategy)?\n3. Performance in various math domains?\n4. How does retrieval quality correlate with final translation quality?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. Unlike AlphaProof and other systems that require manual theorem translation before proof synthesis, Proofbridge addresses the complete translation pipeline end-to-end.\n2. The semantic correctness metric based on bi-directional equivalence.\n3. The paper compares against 10 models like GPT-5-mini, Gemini-2.5, and specialized theorem provers (DeepSeek-Prover, Kimina-Prover), demonstrating significant improvements (+31.14% SC, +1.64% TC at pass@32 over Kimina-Prover-RL-1.7B)\n4. NuminaMath-Lean-PF (38.9k pairs) provides a substantial training resource.", "weaknesses": "1. The paper dismisses FormL4 [1] as \"not released,\" but it looks like it was released a year ago. The paper should provide a more detailed comparison of technical approaches and, if possible, empirical comparison using their published benchmark.\n2. The paper shows that zero-shot actually performs better on SC (40.16% vs. 31.56%), suggesting random few-shot examples hurt performance. This makes the comparison less fair since Proofbridge always uses retrieved (relevant) examples.\n3. No analysis of the judge's reliability for SC Metric, as using an LLM introduces a potential source of unreliability.\n3. It is unclear how this approach would scale to other, more abstract areas like topology and category theory. These proofs are often much longer, rely on a vast library of existing lemmas, and have more complex dependency structures.\n\n[1] Process-Driven Autoformalization in Lean 4 https://github.com/rookie-joe/PDA", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "5HzREXYO3x", "reviewer": "Reviewer_XmYx", "summary": "This paper proposes a novel \"lean code generator\" that translates from natural language statement-proof pairs to formalized statement-proof pairs. This is achieved by first training a joint embedding space of NL and formal proofs by contrastive learning, and then training a RAG translator by supervised finetuning that retrieves relevant formal proofs in the database according to natural language prompts. The retrieval system reports SOTA performance on the recall rate. The RAG translator achieves SOTA performance on both the semantic and compilation correctness.", "questions": "Please refer to the weaknesses.", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1. The paper is well-motivated to address the gap between the power of NL and formal math provers, by translating between natural and formal languages. \n2. The retrieval augmentation has shown compelling performance in the translating accuracy compared to the SFT-only baseline.", "weaknesses": "1. Since existing baselines are limited in both joint embedding learning and FL-NL translation, the paper will benefit from an end-to-end evaluation. It's important to evaluate how SOTA NL prover's ability can be boosted in FL domain by translating their NL proofs to FL proofs. It will be interesting to see if GPT and Gemini-2.5-pro benefits from FL-NL translation and how the resulting performances compare to SOTA FL provers.\n\n2. The translation type correctness for RAG-SFT w/o external repair from Gemini is relatively poor compared to Kimina-prover-RL.  However, the semantic correctness excels by a significant margin.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "8SkCLPzLLv", "reviewer": "Reviewer_9ttn", "summary": "This paper presents ProofBridge, a unified framework for the autoformalization of NL math proofs into Lean4. It contains three main components: (1) a joint embedding model that aligns NL and FL theorems in a shared semantic space; (2) a retrieval-augmented SFT that conditions proof autoformalization; (3) an iterative proof repair mechanism that combines Lean type-checking and semantic equivalence verification. The authors curate two benchmarks: NuminaMath-Lean-PF and MiniF2F-Test-PF for evaluation. Experiment results show improvements over all-MiniLM-L6-v2 on the retrieval task and Kimina-Prover-RL-1.7B in the proof autoformalization task.", "questions": "1. Why was Kimina-Prover-RL-1.7B chosen as the primary baseline instead of larger variants?\n2. What is the out-of-distribution test results or adversarial perturbations results on the retrieval task\n3. What is the performance breakdown across different mathematical domains\n4. Can the authors provide comprehensive qualitative examples showing when and why the framework helps?", "limitations": "", "rating": 2, "confidence": 4, "soundness": 2, "presentation": 1, "contribution": 2, "strengths": "1. This paper presents an interesting proof repair technique by a proof autoformalizer\n2. The experiment indicates the framework performs well in the 1.7B level model\n3. The NuminaMath-Lean-PF contributes a 40k-level dataset of natural language to a formal language autoformalization dataset.", "weaknesses": "Despite the paper’s mentioned strengths, it requires significant revision to address the following cirtical weaknesses:\n\n1. **Overclaiming SOTA:** My primary concern is that the paper claims to outperform previous SOTA models and position itself as the new SOTA. However, the baselines it uses for comparison are clearly not current SOTA methods in either proof retrieval or proof autoformalization tasks. For the retrieval task, all-MiniLM-L6-V2 is an outdated model in 2020. More recent and competitive baselines should be considered, such as Qwen3-Embedding-8B [1]. For the proof autoformalization task, comparing solely against the 1.7B variant of Kimina-Prover is insufficient, as the same work introduces 8B and 72B versions that significantly outperform the 1.7B variant. The overclaiming of SOTA significantly harms the objectivity of the paper. \n2. **Questionable Evaluation Methodology:** The evaluation procedure for proof retrieval is overly idealized and does not adequately reflect real-world complexity. The task assumes that for each NL input, there exists an exact corresponding FL proof in the dataset, and the goal is to simply retrieve this match. However, realistic scenarios are much more complex. For example, there may be many out-of-distribution queries and hard negative samples that require fine-grained discrimination.\n3. **Incomplete experimental analysis:** The experimental section lacks the depth and rigor expected for the conference paper. It misses some important ablation studies, such as the impact of individual components, the effect of retrieval hyperparameters, the analysis of inference hyperparameters, and the impact of training data size and composition. It also lacks qualitative analysis, such as examples of successful and failed retrievals, a qualitative comparison between generated and gold-standard proofs, and case studies on the repair process.\n4. **Poor paper organization and clarity:** The paper suffers from significant structural and clarity issues:\n    1. Structural problems: The NuminaMath-Lean-PF dataset is first mentioned in the methodology section in line 304 without any introduction to its construction and characteristics. Readers must go to Section 5 to find its details.\n    2. Unclear experiment section: The experiment section is difficult to read due to lack of clear subsection organization (such as separate subsections for retrieval results, autoformalization results, ablations, and additional studies). It also mixes the main results and ablation studies, and provides an insufficient description of experimental settings.\n\n[1] Zhang, Y., Li, M., Long, D., Zhang, X., Lin, H., Yang, B., ... & Zhou, J. (2025). Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models. *arXiv preprint arXiv:2506.05176*.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "SUVwKCJgoW", "reviewer": "Reviewer_h6DL", "summary": "This paper presents a framework for automatically translating natural language mathematical theorems and proofs into Lean 4 formal language with RAG. The approach consists of three main components: (1) a joint embedding model that aligns natural and formal language theorem-proof pairs, (2) retrieval-augmented fine-tuning of LLMs, and (3) an iterative repair mechanism that uses Lean's type checker and semantic equivalence verification. The authors demonstrate improvements over baselines on some experiments.", "questions": "Please answer the question in Weakness.", "limitations": "", "rating": 2, "confidence": 4, "soundness": 2, "presentation": 3, "contribution": 2, "strengths": "1. The use of LeanDojo’s ByT5 encoder to capture the \"linearized DAG traversal\" of Lean proofs, rather than just treating the code as flat text. It might be a thoughtful method for encoding the structural properties of formal proofs.\n2. The integration of RAG and SFT is well-executed. The authors provide corresponding ablation studies which help demonstrate the impact of SFT.", "weaknesses": "1. The core motivation of the task, i.e., translating a known natural language proof into a formal proof, is questionable. The primary value of formal math languages is to verify statements whose correctness is uncertain. In most practical scenarios, a formal statement is the starting point, and the proof is the unknown to be found. If an informal proof is already known to be correct, the motivation for formalization becomes unclear. Of course, you can state that it's useful in some scenarios, like translating textbooks and formalizing existing proofs. But currently, what you are claiming is that the previous 2-stage practice (formalize statement and prove in formal language) is problematic, and yours is correct. It's not the case.\n2. The paper claims the superiority of encoding the \"linearized DAG traversal\" using the ByT5 encoder. However, there is no ablation study to support this. How does this compare to a simpler baseline, such as encoding the raw text of the FL proof?\n3. The experimental comparisons in Table 2 are insufficient and potentially misleading: (1) The baseline models were also provided with the full input context, i.e., the NL theorem, the NL proof, and retrieved RAG examples, right? Then the authors should provide ablations that isolate the benefit of the (arguably unrealistic) input. Specifically, how much does adding the NL proof and the RAG component each contribute to the performance of both the baseline and the proposed model? This is crucial to understand if PROOFBRIDGE is genuinely better at using the informal proof, or whatever else. (2) The reported Semantic Correctness for powerful models like Gemini-2.5-Pro and GPT-5-mini seems anomalously low. The authors should provide a case study or a deeper analysis explaining these failures. (3) The paper dismisses Kimina-Autoformalizer for achieving 0% correctness. This is a strawman argument. These models are designed for statement formalization only and to output sorry, not end-to-end proof generation. Stating they \"perform poorly\" is an unfair characterization of models built for a different task.\n4. The work is missing a comparison to REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning (arXiv:2505.20613, 2025), which is highly relevant to this work.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "OOhTw9Z7Aw", "reviewer": "Reviewer_B6B5", "summary": "ProofBridge is a unified framework for directly translating both the statement and proof from natural to formal language. It utilizes an embedding system that projects FL and NL statements to a joint space. This is used as a retriever for the autoformalization model which the authors train using SFT. The model is tested with iterative repair and it demonstrates superior performance in type check rate and semantic correctness compared to baselines.", "questions": "For the same natural language problem, there might exist different correct ways to state it in Lean, some being easier to prove than others. Do the authors envision ProofBridge to be extensible to optimize for downstream provability of formalized statements?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "The task of end-to-end proof autoformalization has, as the authors claim, been underexplored and it is an interesting new problem formulation. It is well-motivated by the difficulty manual formalization, such as during the AlphaProof experiment on IMO 2024 problems. Although there has been existing work on statement or proof autoformalization, an end-to-end approach for both statements and proofs has rarely been explored or evaluated. The experiment results rigorously show the proposed method's advantage over the numerous baselines considered. This paper may serve as a solid baseline for this end-to-end autoformalization setting for the community.\n\nThe presentation of this paper is clear and easy to follow.", "weaknesses": "My biggest concern is that while the problem setting has been underexplored, the method that the authors consider is largely only piecing together existing approaches. The method largely resembles existing work on retrieval-augmented statement autoformalization (see below), with the added complexity that it starts training from Kimina-Prover-1.7B which has been trained for proving already.\n\nContrary to what the authors claim, I think NL/FL joint embedding has been explored in previous work, in the form of first informalizing the FL statement and then embedding NL queries and informalized theorems into a joint space, and retrieving similar FL examples from NL queries at test time for the purpose of statement or proof autoformalization. This was proposed in prior work like [1, 2, 3]. In this paper, the authors proposed a slightly different method that trains linear projections from FL and NL embeddings (based on existing models) into a shared space. Although technically different, I don't see how this is advantageous compared to existing approaches based on informalization which have shown to be effective. Either some explanation or quantitative comparison is needed to demonstrate this.\n\n[1] https://arxiv.org/abs/2403.13310v2\n[2] https://arxiv.org/abs/2410.10878\n[3] https://openreview.net/forum?id=hUb2At2DsQ\n\nThe \"Semantic Correctness\" (SC) evaluation metric is not new. In [1], the BEq metric was introduced which is basically the same as SC. Subsequent work such as RLMEval [2] and StepFun-Formalizer [3] have extended and improved BEq (although I admit the latter should be considered contemporaneous work). Even ignoring BEq, there has been extensive prior work on using an LLM judge as a semantic correctness check. This is a small issue, but I would encourage the authors to recognize the previous work.\n\n[1] https://openreview.net/forum?id=hUb2At2DsQ\n[2] https://arxiv.org/abs/2406.07222\n[3] https://arxiv.org/abs/2508.04440\n\nThe retriever baseline, all-MiniLM-L6-v2, shouldn't be considered a SOTA. That is a small model pretrained on general NL data. I encourage the authors to try a larger pretrained model such as e5-mistral-7b-instruct (which LeanSearch seems to use), or at least not label the current baseline as SOTA (because LeanSearch exists).", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)