Aug 06 2024

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.