LeanAgent repeatedly ingests new Lean repositories, traces theorem and premise data through LeanDojo, updates a dynamic database, progressively retrains premise retrieval and searches for proofs of `sorry` theorems. Successful proofs can be added back to the knowledge base for later learning.
The LeanAgent paper reported formal proofs for 155 theorems whose Lean repositories previously contained missing proofs across 23 repositories, while improving lifelong-learning stability and backward transfer relative to a static theorem-proving baseline.
The work introduced a durable systems perspective for AI theorem proving in which mathematical knowledge, repositories and model competence evolve together, addressing a limitation of provers trained once on static snapshots.
Significance rationale: LeanAgent reframed neural theorem proving as a continual-learning problem over evolving mathematical repositories rather than a fixed benchmark, combining a dynamic knowledge database, curriculum ordering and progressive retriever training to preserve and extend proof capability across domains.
—
The arXiv research record introduced LeanAgent and reported its continual-learning and formal-proof results across multiple Lean repositories.
The public LeanAgent repository exposes implementation, tests and reproduction setup, and the work later appeared at ICLR 2025. Machine-checked describes Lean acceptance of generated formal proofs; it does not imply independent replay of the complete experiment or new informal mathematical results.
No corrections recorded.
