Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.

翻译：定理证明是数学的基础环节，涵盖从自然语言的非形式化推理到形式化系统中的严格推导。近年来，深度学习技术的进步，尤其是大语言模型的出现，引发了利用这些技术改进定理证明过程的研究热潮。本文对深度学习在定理证明中的应用进行了全面综述，具体包括：（i）系统梳理了自动形式化、前提选择、证明步骤生成及证明搜索等各类任务中的现有方法；（ii）详尽总结了现有精编数据集及合成数据生成策略；（iii）深入分析了评估指标与前沿方法的性能表现；（iv）批判性探讨了当前面临的持续挑战及未来探索的潜在方向。本综述旨在为定理证明中的深度学习方法提供基础性参考，以激发并推动这一快速发展领域的后续研究。相关论文精选列表可在 https://github.com/zhaoyu-li/DL4TP 获取。