Abstract: Automating theorem proving has long been one of the core challenges in mathematics and computer science. It aims to enable machines to (semi-)automatically generate proofs of formal theorems, and has important application prospects in areas such as mathematical theorem proving and software verification. Recent progress has shown that intelligent techniques represented by large language models can effectively generate formal proofs in certain domains, and have demonstrated human-expert-level performance in the International Mathematical Olympiad. This provides a new pathway for addressing the challenge of theorem proving. This article aims to review the recent status of theorem proving based on intelligent techniques. Specifically, this article first introduces the basic classifications and approaches of classical theorem provers, and covers recent progress in intelligent theorem proving from three aspects: autoformalization, premise selection, and proof generation. Then, this article introduces several representative theorem proving systems, as well as the application of theorem proving techniques in the field of software verification. Finally, this article discusses the main challenges currently faced by theorem proving and outlines future research directions.