AI 辅助庞加莱猜想的 Lean 形式化

摘要

我们提出了庞加莱猜想的 AI 辅助 Lean 4 形式化。该项目始于有限的可重用正式基础设施，用于证明背后的几何分析。为了组织这项工作，我们将数学家准备的证明蓝图与明确的里程碑陈述结合起来。这些里程碑使得智能体并行工作成为可能，并为数学家提供了明确的要点来定位阻碍因素并提供有效的数学指导。我们的分析确定了此工作流程背后的人为干预和组织选择。该项目为未来正规化项目提供了可重复使用基础设施的起点；这种基础设施一旦开发出来，最终可以降低验证几何分析中数学结果的成本。

AI 辅助庞加莱猜想的 Lean 形式化：论文原图 — 图 1：将数学目标转换为经过验证的精益形式化的工作流程。实线箭头表示工作的正常进展。虚线箭头表示被阻止的任务可以返回源收集、语句修订或进一步分解。人类决策决定数学范围、审查优先级和验收标准，而智能体则协助源分析、形式化、监控和诊断。