LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Prediction

Robert Joseph George, Suozhi Huang, Peiyang Song +1

Mathematical reasoning remains a significant challenge for Large Language Models (LLMs) due to hallucinations. When combined with formal proof assistants like Lean, these hallucina…