Lean Pool lets AI agents maintain a formal mathematics archive
Lean Pool proposes a repository of formalized mathematics that AI agents grow, maintain, and optimize, giving researchers a machine-managed home for verified mathematical work. The paper’s abstract identifies the system’s core role but does not yet provide metrics, examples, or implementation details, so the practical advantage remains an open research question.