LeanDojo-v2: A full loop for training and testing Lean 4 provers

If you are building AI assistance for Lean 4, generating a tactic suggestion in isolation is rarely the hard part. You also need a traceable corpus, a way to replay proof states, and a training loop that can be rerun as repositories change. LeanDojo-v2 is structured around that loop. The project describes itself as an end-to-end framework for training, evaluating, and deploying AI-assisted theorem provers for Lean 4. It extends the original LeanDojo stack with the LeanAgent lifelong learning pipeline and combines repository tracing, lifelong dataset management, retrieval-augmented agents, Hugging Face fine-tuning, and external inference APIs in one toolkit. In practice, the README outlines a sequence: clone Lean repositories from GitHub or local paths and trace them with Lean instrumentation, store structured theorem information in a dynamic database, train agent policies with supervised fine-tuning, GRPO-style reinforcement learning, or retrieval objectives, drive Pantograph-based provers to fill sorrys or verify solutions, and use the Hugging Face API for large-model inference. Modular by design The codebase separates concerns so teams can adopt parts without taking the whole stack. A tracing pipeline can be reused without the agents, custom trainers can be swapped in, and an external inference service can be stood up through the API layer. Agents: BaseAgent orchestrates repository setup, training, and