发表机构
Peking University; Beijing Normal University; Capital Normal University; New Cornerstone Science Laboratory; Center for Machine Learning Research, Peking University; Great Bay University; Zhongguancun Academy（北京大学; 北京师范大学; 首都师范大学; 新基石科学实验室; 北京大学机器学习研究中心; 大湾区大学; 中关村学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一个由人工智能辅助的 Lean 4 形式化庞加莱猜想项目，通过结合数学家准备的证明蓝图与明确的里程碑陈述，支持并行智能体工作并便于数学家提供指导，为未来形式化项目提供可重用基础设施，以降低验证几何分析数学结果的成本。
AI 中文摘要
我们提出了一个由人工智能辅助的 Lean 4 形式化庞加莱猜想的工作。该项目始于对证明背后几何分析的可重用形式化基础设施有限的情况。为了组织这项工作，我们将数学家准备的证明蓝图与明确的里程碑陈述相结合。这些里程碑使得并行智能体工作成为可能，并为数学家提供了明确的定位障碍点并提供有效数学指导的切入点。我们的分析识别了该工作流程背后的人工干预和组织选择。该项目为未来形式化项目迈向可重用基础设施提供了一个起点；此类基础设施一旦开发完成，最终可能降低验证几何分析中数学结果的成本。
英文摘要
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.
Comments15 pages, 2 figures. Code: https://github.com/frenzymath/PoincareConjecture
