我们在 Lean 4 中实现了对庞加莱猜想的形式化证明，并在整个过程里引入了 AI 辅助。项目起始时几乎没有可复用的几何分析形式化基础，为此我们先搭建了底层框架。随后，数学家提供了一份详细的证明蓝图，并将关键步骤拆解为若干里程碑声明。每个里程碑既是 AI 代理并行工作的目标，也为数学家指明了可能的阻塞点，从而能够及时提供针对性的数学指导。我们的分析揭示了人类干预的具体形式以及组织上的关键决策，这些经验对后续的大规模形式化项目具有参考价值。该工作为未来几何分析领域的可复用形式化基础设施奠定了起点，若进一步完善，预计能够显著降低验证数学结果的成本。
点评