Mathematical work supported
LeanAgent orders Lean repositories into a learning curriculum, traces their proofs and premises, progressively trains a retriever, and searches for proofs of declarations containing sorry. Successful proofs enter a persistent database and can be proposed to repository maintainers. This is a close precedent for a mathematical library that grows during a learning process. Paper, §§3–4.
Architecture and provenance
The demonstrated learning component is a progressively trained retriever initialized from ReProver. The experiments use ReProver’s tactic generator with best-first proof search. Broader compatibility with other language models is a design claim; the paper explains that using whole-proof models would require architectural changes. Paper, §3.3 and Appendix A.1.
The database stores repository URLs and commits, Lean versions, theorem positions and statements, traced tactics, premises, and proof status. The Theorem and Repository structures in dynamic_database.py confirm source provenance and status categories. It would be false to call LeanAgent provenance-blind. The paper also describes file-import accessibility filtering for retrieval. A module-accessibility graph should not be confused with a complete proof-dependency or logical-strength graph. Source.
Evaluation
The paper evaluates proof search and retrieval across selected Lean repositories against its ReProver starting point. Filling a sorry supplies a missing formal proof in that repository; it does not establish new mathematics. Retrieval recall and end-to-end proof success are different measurements. The experiments were not rerun for this comparison. Paper, §4 and Appendix A.7.
Comparison with Axeyum
LeanAgent supplies direct prior art for database growth, curriculum selection, retriever improvement, and proof reuse. Axeyum should not use a static-library caricature to distinguish its recursive-improvement vision.
Axeyum’s comparison concerns heterogeneous evidence routes and mathematical applicability. Its native and imported proofs, CAS records, explicit constructive data, and axiom footprints introduce selection requirements beyond retrieving accessible Lean premises. The reviewed LeanAgent database does not itself establish a policy for choosing among those heterogeneous routes. That is a scoped observation about the reviewed structures, not a universal absence claim. Axeyum must demonstrate that its selector actually consumes such distinctions before claiming a working advantage.
Two reasons a later proof may succeed
Suppose an agent fails to prove a theorem because it does not find a useful lemma. Later, its database contains an additional result and its retriever has been trained on another repository. A second attempt succeeds.
The new result may have made the proof possible. Better retrieval may have made an existing proof route easier to find. Both changes may have contributed. A growing system needs experiments that distinguish them. One comparison keeps the model fixed while the library grows. Another holds the available library fixed while the retriever changes. This is a proposed evaluation pattern for Axeyum, not a claim that LeanAgent ran exactly those ablations.
Provenance makes that experiment reproducible. The record must identify which repository versions, premises, and model checkpoint each attempt could use. An accepted proof must also satisfy the target environment’s requirements. Source provenance alone does not settle the status of every transitive assumption.
Mathematical applicability
Axeyum’s constructive statement families add another selection question. A retrieved theorem may guarantee an approximate root when the task requires an exact one. Another theorem may provide an exact root only under a quantitative hypothesis that has not been established. Similarity to the goal is useful, but it cannot settle those obligations.
The engineering objective is to combine retrieval with explicit applicability checks and accepted evidence. Ωmega provides an earlier proof-planning comparison. MMT and MathHub provide a comparison for the representation of mathematical knowledge across contexts.
The Axeyum comparison refers to its documented source snapshot. Repository structure and paper descriptions were reviewed; no comparative benchmark was run.