LeanAgent 提出 lifelong learning formal prover：跨 23 个 Lean 仓库持续学习并证明 155 个此前未被人类形式化证明的定理

LeanAgent 将 formal theorem proving 从静态 benchmark fine-tuning 推向 lifelong learning：系统用 curriculum learning、动态知识库与 progressive training 在不断扩展的 Lean repositories 上持续学习，同时避免 catastrophic forgetting。论文报告在 23 个 Lean repositories 中成功证明 155 个此前未被人类 formal proof 覆盖的 theorem，涉及 abstract algebra、algebraic topology 等较高级领域，并展示 backward transfer。