arXiv：cs.AI· Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong·· 5 小时前AI 评分70
arXiv 论文：AI 辅助完成庞加莱猜想的 Lean 4 形式化
An AI-Assisted Formalization of the Poincar\'e Conjecture
AI 导读
论文报告了庞加莱猜想的 AI 辅助 Lean 4 形式化。由于几何分析相关的可复用形式化基础设施有限，团队将数学家准备的证明蓝图与明确的里程碑声明结合，使多个智能体并行工作，并让数学家能定位阻塞点、提供有效数学指导。论文分析了这一工作流背后的人工干预与组织选择，认为其可作为未来形式化项目可复用基础设施的起点，这类基础设施一旦成熟，有望降低验证几何分析结果的成本。
正文
Abstract:We present an AI-assisted Lean 4 formalization of the Poincaré conjecture. The project began with limited reusable formal infrastructure for the geometric analysis behind the proof. To organize this work, we combined a proof blueprint prepared by mathematicians with explicit milestone statements. These milestones enabled parallel agent work and gave mathematicians clear points to locate blockers and provide effective mathematical guidance. Our analysis identifies the human interventions and organizational choices behind this workflow. The project provides a starting point toward reusable infrastructure for future formalization projects; such infrastructure, once developed, could eventually reduce the cost of verifying mathematical results in geometric analysis.
| Comments: | 15 pages, 2 figures. Code: this https URL |
| Subjects: | Artificial Intelligence (cs.AI); Geometric Topology (math.GT) |
| Cite as: | arXiv:2610.08329 [cs.AI] |
| (or arXiv:2610.08329v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.08329 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Leheng Chen [view email]
[v1]
Tue, 6 Oct 2026 13:27:51 UTC (2,799 KB)
来源：arXiv：cs.AI · arxiv.org