Generating Millions Of Lean Theorems With Proofs By Exploring State Transition Graphs

David Yin, Jing Gao

Large Language Models (LLMs) have demonstrated significant potential in generating mathematical proofs. However, a persistent challenge is that LLMs occasionally make mistakes, whi…