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 中完成了庞加莱猜想的形式化，项目起点是几何分析证明所需可复用形式化基础设施有限。他们把数学家准备的证明蓝图与明确的里程碑陈述结合，使多个智能体可以并行工作，也让数学家能定位阻塞点并给出数学指导。论文分析了这一流程中的人工介入与组织选择，并称该工作为未来形式化项目提供了可复用基础设施的起点。
正文 · AI 翻译
摘要：我们提出了一个 AI 辅助的庞加莱猜想 Lean 4 形式化。该项目开始时，证明背后的几何分析可复用形式化基础设施十分有限。为了组织这项工作，我们将数学家编写的证明蓝图与明确的里程碑陈述结合起来。这些里程碑使多个智能体能够并行工作，并为数学家提供了清晰的定位点，以便发现阻碍并提供有效的数学指导。我们的分析识别了这一工作流程背后的人工干预和组织选择。该项目为未来形式化项目的可复用基础设施提供了一个起点；此类基础设施一旦开发出来，最终可以降低几何分析中数学结果的验证成本。
| 评论： | 15 页，2 幅图。代码：此 https URL |
| 主题： | 人工智能（cs.AI）；几何拓扑（math.GT） |
| 引用为： | arXiv:2610.08329 [cs.AI] |
| （或 arXiv:2610.08329v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.08329 arXiv 颁发的 DOI 通过 DataCite（待注册） |
提交历史
发件人：Leheng Chen [查看电子邮件]
[v1]
2026 年 10 月 6 日星期二 13:27:51 UTC（2,799 KB）
来源：arXiv cs.AI · arxiv.org