Lean Pool：用 AI 智能体维护的形式化数学档案

arXiv 上线了一篇关于「Lean Pool」的论文，介绍了一个由 AI 智能体持续维护的形式化数学档案仓库。该仓库并非由人工手动补充，而是由智能体自动「生长」、整理与优化其收录的形式化数学内容。

项目背景

Lean 是一类广泛应用于形式化数学与程序验证的交互式定理证明器。随着社区贡献者数量增加，形式化数学资料分散在多个项目之中，缺乏统一的整理与索引，给后续研究者带来较高检索成本。Lean Pool 的目标是借助 AI 智能体对分散的形式化数学项目进行统一收纳与持续维护。

核心机制

根据论文摘要，Lean Pool 的关键特点是：

• 仓库的内容由 AI 智能体自动增长，而非完全依赖人工提交；
• 智能体负责日常维护，包括对已有内容的更新与修正；
• 智能体对仓库进行优化，以提升可检索性与可用性。

论文还包含一份导入项目目录（catalogue of imported projects），用于展示已被纳入 Lean Pool 的形式化数学项目列表。

论文信息

• 作者：Vasily Ilin
• 篇幅：52 页，含 6 张图表
• 提交时间：2026 年 9 月 21 日（v1）
• 分类：cs.AI（人工智能）
• DOI：10.48550/arXiv.2609.25199

意义与局限

Lean Pool 把「AI 智能体」从单次定理证明或对话交互，拓展到对长期知识库的自主维护，体现了一种新的 agent 应用形态：对结构化知识仓库的持续运营，而非一次性任务完成。这对形式化数学社区具有工具价值，也对 AI 智能体在长周期、版本化数据上的可靠性研究提供了参考场景。不过目前披露的信息仍以摘要为主，仓库的具体规模、覆盖项目数量、智能体架构与评测指标等关键细节，需要等待论文全文与项目开源情况进一步公布。