跳转至

文章背景与核心概要

形式化数学通过交互式定理证明器将深奥严密的数学证明转化为计算机可严格验证的代码，但传统形式化数学库的扩充极度依赖顶尖数学家的手工编写，人力维护成本高昂且发展进程相对缓慢。为了突破这一制约形式化数学规模化演进的长期瓶颈，研究者 Vasily Ilin 提出了 Lean Pool 这一开创性架构，旨在构建一个完全由 AI 智能体 (AI Agent) 自主扩充、日常维护与深度优化的形式化数学资源池。该项目依托现代定理证明框架 Lean 4，巧妙架起了前沿人工智能与形式化符号推理之间的桥梁，探索了智能体自动生成证明、跨项目整合知识与持续重构代码的全新范式。这一突破不仅为自动化数学发现与大规模可靠知识库的协同构建指明了方向，也标志着形式化数学正式迈向由 AI 自主驱动的智能化演进新阶段。

Lean Pool：由 AI 智能体自主维护与持续扩充的形式化数学知识库

Lean Pool: An AI-Maintained Archive of Formalized Mathematics

内容概要

Summary

Lean Pool 是一个动态演进的形式化数学知识库，完全由 AI 智能体 (AI Agent) 自主进行扩充、日常维护与深度优化。该项目由 Vasily Ilin 提出，在 Lean 形式化框架内搭建起连接人工智能与自动定理证明的桥梁。

Lean Pool is a dynamic repository of formalized mathematics that is autonomously grown, maintained, and optimized by AI agents. Proposed by Vasily Ilin, the project bridges artificial intelligence and automated theorem proving within the Lean framework.

论文元数据

Paper Metadata

属性 详情
标题 Lean Pool: An AI-Maintained Archive of Formalized Mathematics
作者 Vasily Ilin
主要学科领域 人工智能 (cs.AI)
提交日期 2026 年 9 月 21 日
arXiv 编号 arXiv:2609.25199
**数字对象标识符 (DOI) ** 10.48550/arXiv.2609.25199
备注信息 共 52 页，含 6 幅图。包含已导入项目的目录列表。
Attribute Details
Title Lean Pool: An AI-Maintained Archive of Formalized Mathematics
Authors Vasily Ilin
Primary Subject Artificial Intelligence (cs.AI)
Submitted on September 21, 2026
arXiv Identifier arXiv:2609.25199
DOI 10.48550/arXiv.2609.25199
Comments 52 pages, 6 figures. Includes a catalogue of imported projects.

论文摘要

Abstract

Lean Pool 是一个形式化数学知识库，完全由 AI 智能体负责自主扩充、日常维护与持续优化。

Lean Pool is a repository of formalized mathematics. It is grown, maintained and optimized by AI agents.

访问链接与相关资源