Formal Theorem Proving with Lean World Models

Most recent neural provers write a whole formal proof before Lean checks it, so they run open-loop: without intermediate observations, a wrong assumption about the proof state can derail the attempt. Many also use informal reasoning distilled from larger, more expensive models before writing Lean proofs. We propose to train a Lean world model, where the prover predicts Lean's goal states and error messages alongside its proof steps, learning explicit Lean-level reasoning from Lean's feedback rather than from a large LLM teacher. Because it predicts errors, it can repair a proof within the same response, using the failed attempt and its predicted diagnosis. We train 4B and 8B Qwen3 models by supervised fine-tuning on feedback-annotated proofs followed by reinforcement learning (GRPO), and compare them with a standard prover trained through the same stages without Lean annotations. The 8B world-model prover outperforms the standard prover, reaching 75.61% pass@32 on miniF2F and 16.44% on ProofNet against 71.31% and 13.21%. Without informal reasoning, the world-model prover solves as many miniF2F problems as the standard prover further trained on teacher-written reasoning. Adding informal reasoning raises its miniF2F pass@32 to 77.05%, above DeepSeek-Prover-V2-7B and below Goedel-Prover-V2-8B, whose post-training techniques could complement our focus on learning from Lean's feedback.