arXiv cs.AI· Zhiyuan Zhang, Axel Delaval, Leheng Chen, Jinxuan Chen, Jie Xu, Yuxuan Liao, Jiedong Jiang, Chunlei Liu, Bin Dong·· 10 天前AI 评分54
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