Lean Pool:一个由 AI 维护的形式化数学档案库

TL;DR Lean Pool 是一个由 AI 智能体持续扩充、维护与优化的形式化数学仓库，用 Lean 内核保证证明正确，绕过 Mathlib 人工审核瓶颈，为 AI 生成数学证明提供可复用基础。

问题

问题背景

形式化数学与 AI 自动定理证明领域，近年因大型语言模型（LLM）生成证明能力提升而备受关注。Lean 已成为验证数学证明的主流语言，但形式化数学库的构建仍高度依赖人工审核。

现有方法局限

Mathlib 等标准库采用严格人工审核，增长速率线性，难以覆盖研究级数学所需的定义与定理。AI 生成的证明虽可由 Lean 内核校验正确性，但库中缺少必要前置定义和引理，导致大量生成内容无法接入现有形式化体系。人工审核的吞吐量远低于生成吞吐量，形成验证瓶颈。此外，定义与定理陈述的质量、跨版本依赖兼容性、编译速度与 RAM 占用等维护任务仍主要靠人，无法支撑规模化扩展。

为什么这个问题难/重要

验证是生成商品化后的关键瓶颈：证明正确性可由内核保证，但定义与定理陈述的语义质量、库结构的可读性与可发现性、跨版本升级稳健性等仍需持续投入。自动化维护必须在严格 lint、LLM 评审与内核验证之间取得平衡，避免低质量形式化污染库，同时不牺牲可追溯性。业界关注形式化作为可信 AI 推理基础设施的价值，但库覆盖不足与维护成本高企制约自动定理证明在生产环境中的落地。

行业类比

类似软件工程中 AI 生成代码入库：CI 管线保证可运行性，但代码库的语义质量、依赖兼容与重构优化仍需机器人持续维护与审阅，才能支撑大规模协作。

核心洞察

• 将 AI 代理从“证明生成器”重新定位为“数学库的持续维护者”，解决形式化验证基础设施的线性增长瓶颈。现有 AI for Math 工作多聚焦单一定理证明或自然语言到形式化的翻译（如 GPT-f、LeanDojo），而 Lean Pool 让 AI 代理负责发现 Apache-2.0 项目、执行 lint、缩短证明、优化编译速度与 RAM 使用，形成闭环维护流水线。这直接回击 Mathlib 因严格人工审查而增长缓慢的痛点，把稀缺的验证能力产品化为自动化的基础设施，对任何依赖高质量版本库的团队都有工程借鉴意义。
• 利用 Lean kernel 的正确性保证作为自动质量门禁，叠加 LLM 对定义与定理语义的审查，构建“两层验证”机制。传统形式化库依赖人工 review 保证可用性，耗时且主观；Lean Pool 则让 kernel 负责证明不可错（机器可验证），LLM 评估定义和定理的语义恰当性（需人类判断），二者分层。这种信任模型与纯 LLM 生成有本质区别，既保留形式验证的严谨性，又大幅提升维护吞吐量，为其他需要高可靠性的 AI 生成内容（如代码库、规范文档）提供了可复用的工程范式。

方法

输入

Lean Pool 的构建与扩展以两类输入为主：一是社区或 AI 发现的形式化数学项目（主要来自 Apache-2.0 许可的开源仓库），二是针对现有库中新定义、新定理的补丁与优化提案。

关键模块

1. AI 代理采集与整合
   • 定期扫描开源生态，发现可导入的形式化成果，自动提取其中的定义、定理和证明，并适配 Lean Pool 的目录结构与依赖。
2. 质量保障
   • 证明正确性：由 Lean 内核对所有证明进行形式化验证，保证零逻辑错误。
   • 代码规范：使用严格 linter 检查命名、模块划分、行长度等风格问题。
   • 语义审查：LLM 审查新定义和定理陈述，评估其数学意义、复用潜力及与现有内容的冗余，决定接纳或拒绝。
3. 自动维护与优化
   • 证明压缩：定期运行自动化工具，缩短冗长证明，提升可读性与编译速度。
   • 编译与内存优化：重构模块依赖、调整声明顺序、使用更高效的数据结构，降低构建资源消耗。
   • 兼容性维护：监控上游 Lean 版本和依赖库的变更，自动生成迁移补丁，保持稳定版本可编译。
4. 持续集成与流水线
   • CI 包含 archive-specific 规则、profiling 和性能回归测试。
   • 每日任务负责贡献者提交的合并、文档更新与发布管线。

输出

产出一个由 AI 持续维护、证明经过内核验证、内容经 LLM 审查的高质量形式化数学库，可直接用于研究级数学的形式化与复用。

差异点：与 Mathlib 依赖人工审查、线性增长不同，Lean Pool 用 AI 代理完成大部分采集、审查和优化工作，实现自动化扩展与性能调优，形成 AI 原生的形式化数学生态。

实验

实验设计

Lean Pool 作为持续演化的形式化数学归档，实验方式与常规基准测试不同：它将 AI 代理 的维护行为视为一个可观测的工程系统。作者在附录 A–C 中记录了观察范围与测量方法，包括集合组成、构建资源对比和 CI 剖析。核心变量是代理驱动的增长 vs. 人工审核下的 Mathlib 线性增长；观测指标包括编译时间、RAM 占用、证明简洁度与库规模。

关键发现

• Lean kernel 保证了证明正确性，严格的 linter 与 LLM 审查用于约束定义和定理陈述质量。
• 代码库定期针对简洁性、编译速度和 RAM 使用率进行优化。
• 归档通过两种方式增长：AI 代理发现 Apache-2.0 或其他许可的形式化项目纳入；社区贡献与持续集成协同。
• 附录提及 价格核算 与 生产审查，暗示可量化的维护成本与代理决策一致性。

与基线的深度解读

Mathlib 因严格人工审核呈线性增长，而 Lean Pool 的 AI 维护模式试图将生成规模化与验证瓶颈解耦。工程启示在于：当生成被商品化后，验证成为瓶颈；Lean Pool 把验证责任拆分为内核（强制正确性）和代理层（维护质量与优化），而不是完全依赖人工 review。与 Mathlib 的关键差异是维护者由人转变为 AI 代理，但仍保留 Lean 内核作为最终仲裁者。这种设计为大规模形式化数学基础设施提供了一种可行的自动化维护范式。

行业影响

落地场景

Lean Pool 提供的 AI 维护形式化数学库能力，可直接用于自动化定理证明平台、软件/智能合约形式化验证服务，以及数学教育中的自动证明批改。在 Lean 生态中，它可作为 Mathlib 的补充层，持续扩展研究级数学定义与定理，降低人工形式化门槛。

商业价值

核心降本点在于大幅减少专家人工审查成本：传统形式化库依赖线性增长的严格人工 review，而 AI agents 可并行发现、整理、优化证明，将边际成本从专家小时数转为算力消耗。同时通过缩短证明和优化编译速度，直接降低 CI 构建资源消耗。商业上可形成形式化验证 SaaS，按证明量或计算资源计费，服务于对正确性有强需求的高价值场景。

与现有产品/工作流的接口

项目以 Git 仓库 + CI 形式提供，可无缝嵌入已有 GitHub Actions、VS Code Lean 插件、AI 代码助手（如 Copilot 类工具）。通过 lake build 与 linting 规则接入现有 Lean 项目，迁移成本低。可考虑输出 API 供其他工具查询定理、复用证明片段。

具体落地 use case

1. 智能合约审计：金融场景中，用 Lean Pool 维护的数学库对 DeFi 合约的核心计算逻辑（如自动做市曲线、清算规则）做形式化验证，AI agents 自动生成并维护证明，审计公司按次调用并出具 kernel 级正确性报告，替代部分人工审计。
2. 电商规则引擎验证：大型电商平台的促销/优惠叠加规则易出现组合爆炸，可将规则翻译为 Lean 命题，利用 Lean Pool 的定理库自动证明其满足价格一致性、不变量等性质，在每次规则变更时由 CI 触发证明更新，降低线上资损风险。

局限

• - **依赖 LLM 审查和 linters 的质量保障机制尚未被充分验证**：论文自述人类写作部分仅一页，主要贡献由 AI 生成，这引发对 Lean Pool 核心机制缺乏深度人工分析和实验验证的担忧。Lean 内核虽保证证明正确性，但定义与定理陈述的质量（命名、抽象层次、与 Mathlib 兼容性）依赖 LLM 审查，而 LLM 审查本身可能产生错误、偏见，且难以量化评估。论文未提供充分对照实验证明 AI 维护的库在质量上能与人工维护的 Mathlib 相媲美，也未论证其长期可持续性。
• - **与 Mathlib 的兼容性维护和依赖演化存在不确定性**：正文提到 “Maintaining compatibility as dependencies evolve”，说明 Lean Pool 需随 Lean 版本与 Mathlib 更新而调整，但自动化兼容维护的成功率与失败模式未明确。AI 代理能否及时、正确处理版本迁移与依赖冲突尚存疑问，且未与 Mathlib 的更新频率和稳定性进行对比。若 Lean Pool 频繁过时或需要大量人工干预，其自动化优势将大打折扣，因此其实用性有待进一步检验。
• - **自动化优化可能牺牲可读性与教学价值**：Lean Pool 定期优化简洁性、编译速度和 RAM 使用，但这些优化可能以牺牲证明的可读性和教学价值为代价。形式化数学库不仅是验证工具，也是人类学习资源。若 AI 生成的证明过于精简或使用非直观技巧，可能降低社区贡献者参与度和理解力。此外，AI 代理生成的定义可能缺乏人类数学家的直觉与领域知识，导致抽象层次不合理，影响库的整体结构质量。