Lean Pool：由AI智能体自主维护与优化的形式化数学代码库
Lean Pool 是一个形式化数学代码库，其核心特色在于完全由 AI 智能体负责拓展、维护与持续优化。该项目展示了人工智能在形式化定理证明与复杂数学知识归档中的自主管理潜力，有助于提高数学形式化库的组织效率与代码质量。由于原论文摘要提供的信息极为简略，具体的智能体协作机制与工程实现细节仍有待进一步公开。
推荐理由展示了利用 AI 智能体自主构建与维护形式化数学库的新探索路径。
原标题：Lean Pool: An AI-Maintained Archive of Formalized Mathematics
阅读 arXiv 人工智能 原文 ↗