Automated Conjecturing and Theorem Finding: A Survey

Automated conjecturing and theorem finding represents a fundamental challenge in artificial intelligence, involving the systematic generation of mathematical conjectures and theorems from given axioms and definitions. This survey provides an overview of automated conjecturing and theorem finding methods. We categorize existing approaches into symbolic methods and data-driven methods. Symbolic methods, which include top-down lemma discovery and bottom-up theory exploration, leverage deductive reasoning and symbolic enumeration. Data-driven methods comprise statistical analogy learning and recent neural methods based on large language models, which learn patterns from large formal corpora, and also include efforts in scientific discovery from experimental data and theorem generation for synthetic data. We also discuss strategies and evaluation methods of interestingness. Finally, we identify current challenges and suggest some future research directions. This comprehensive analysis aims to guide researchers in understanding the current state of automated conjecturing and identifying opportunities for advancing this critical area of mechanized mathematics and automated reasoning.