Tool-Assisted Multi-Turn Theorem Proving with LLMs

We present an approach for training language models to interactively prove theorems using the Lean proof assistant. Our approach enables models to propose partial proofs, receive verification feedback, and iteratively refine their proofs. We develop a synthetic data generation pipeline that converts static proof datasets into multi-turn interactive sequences, complete with incremental verification feedback. Our pipeline also incorporates error recovery examples that teach models to identify and correct mistakes based on verification results. Models fine-tuned on this synthetic data demonstrate improvements over base models, showing increased success rates in proof completion and improved ability to leverage verification feedback.