Lean Pool 提出由 AI agents 持续维护的形式化数学档案库

Lean Pool 是一个用于保存已完成 Lean 4 形式化项目的开放仓库，论文将其定位为由 AI agents 增长、维护和优化的形式化数学 archive。项目处在 Mathlib 的统一库模式与单纯 registry 之间，持续维护独立 formalization projects，并提供搜索、文档与兼容性维护等能力。