Lean Pool 上线，AI 智能体全流程维护数学仓库

数学家 Vasily Ilin 发布 Lean Pool，一个 Lean 形式化数学的精选档案库，号称目前最大。其特别之处在于仓库的生长、维护与优化完全由 AI 智能体完成，仅论文部分由人类撰写。这一项目被视为「AI 自主维护人类知识库」方向的重要尝试。

2026-09-23 ~ 2026-09-23 · 2 条相关

• Lean Pool:全部由 AI 智能体构建和维护的形式化数学仓库上线 — Vasily Ilin · 2026-09-23
• Lean Pool：AI 智能体全流程维护的最大形式化数学仓库 — burny_tech · 2026-09-23