Abstract: Pre-trained language models(PLMs) have demonstrated considerable potential in proving theorems within formal environments such as Metamath.However,this potential remains difficult to translate into reliable reasoning ability.Existing approaches typically require PLMs to directly predict substitutions,which come from an open and potentially infinite expression space.The absence of logical constraints in this process limits the generalization capability of the models.To address this challenge,a new proof paradigm is introduced:work variables temporarily substitute concrete terms during inference,and their specific instances are derived through the unification algorithm.This design enables the model to focus on theorem selection rather than generating unguided substitutions.Based on this paradigm,a dataset is extracted from the Metamath library to construct UnPro-ver(Unification-Driven Prover),which is trained on this data.In addition,several data augmentation strategies are designed to further enhance UnProver’s performance.Experimental results show that UnProver consistently outperforms baseline methods and GPT-4o on test sets,achieving superior performance in both proving capability and efficiency.Moreover,UnProver discove-ries six new and shorter proofs,which have been formally accepted into the official Metamath library.

Key words: Language models, Theorem proving, Metamath, Unification, Work variables