在数学形式化证明的浪潮中，一个关键却被忽视的环节正浮出水面：策略草稿的生成。当前多数讨论聚焦于 AI 如何自动化完成完整证明或诊断错误，却忽略了证明过程中最富创造性的初始阶段 —— 策略构思。本文提出一种下沉至 “策略草稿” 层级的人机协作框架，借鉴陶哲轩近期实验的核心思想，让 Claude 等大模型扮演 “策略展开助手” 而非 “全自动证明引擎”，从而在释放 AI 效率的同时，确保人类专家对证明方向与正确性的最终掌控。
陶哲轩的实验为我们提供了宝贵的原型：他将合作者 Bruno LeFloch 提供的一页纸证明草稿，逐行拆解为微小的逻辑单元，交由 GitHub Copilot 生成 Lean 代码骨架，再亲自验证并填补细节。这一过程耗时仅 33 分钟，远低于传统手动编码，且最终产物具备人类可读性。其精髓不在于 AI 的 “全自动”，而在于 “半自动化” 的分工 —— 人类负责提供高层策略草稿（即那页纸的核心思路），AI 负责将其翻译为形式化语言的技术细节。这种模式成功的关键在于，它将 AI 的强项（模式匹配、语法生成、繁琐计算）与人类的强项（概念理解、策略验证、错误校正）进行了精准切割。
基于此，我们为 Claude 设计一个聚焦于 “策略草稿生成与展开” 的协作框架。该框架的核心原则是：人类专家首先构思并提供一份高层级的、非形式化的证明策略草稿。这份草稿不必完美，甚至可以是模糊的直觉或类比，但它必须包含关键的 “路标”，例如：“尝试使用 ε/2 技巧”、“考虑引入辅助函数 S (x,z)”、“此处需应用三角不等式”。Claude 的任务不是从零开始发明策略，而是接收这份草稿，并将其 “展开” 为更详细、更具操作性的次级步骤列表或伪代码骨架。例如，当人类输入 “尝试使用 ε/2 技巧” 时，Claude 应能生成类似 “设 ε₁ = ε/2, ε₂ = ε/2；分别对 f 和 g 应用极限定义，得到 δ₁和 δ₂；取 δ = min (δ₁, δ₂)” 的详细步骤。这本质上是将人类的策略意图 “编译” 为机器可执行的指令草案。
为了确保这一过程的可靠性与可落地性，我们必须为 Claude 的输出设置严格的 “可验证性” 参数与校验清单。首先，Claude 生成的每一个次级步骤都必须附带其来源依据，即它是由人类草稿中的哪一句策略推导而来。这建立了清晰的追溯链条。其次，框架应强制 Claude 在输出中显式标注其 “置信度” 或 “风险点”。例如，对于涉及特定数学引理（如绝对值不等式 abs_mul）的步骤，Claude 应标注 “此步依赖引理 X，需人工确认其在当前上下文可用”。陶哲轩在实验中就曾遭遇 Copilot “幻觉” 出不存在的策略（如 sub subanc）或错误应用引理的情况，这警示我们必须将风险显性化。最后，人类专家的验证环节必须包含一个强制性的 “反向推导” 检查：随机选取 Claude 生成的 2-3 个关键步骤，要求其反向解释该步骤如何服务于最初的人类策略目标。这能有效防止 AI 在展开过程中 “跑偏” 或引入无关的复杂性。
该框架的落地实施需要一套简单但严谨的工程化清单。第一，输入规范：人类策略草稿应以编号列表或要点形式提供，每个要点应尽可能包含动词（如 “应用”、“构造”、“假设”）和关键对象（如 “ε/2”、“辅助函数”）。避免模糊的形容词。第二，输出模板：Claude 的响应必须遵循 “策略来源 -> 展开步骤 -> 风险标注” 的三段式结构。第三，验证协议：人类专家需在接收输出后，首先检查风险标注，然后执行 “反向推导” 抽查，最后才进行细节填充。这一协议将验证成本控制在可接受范围内，同时最大化安全保障。第四，回滚策略：若在验证中发现 Claude 的展开存在根本性错误或引入不可控复杂性，应立即丢弃该次输出，由人类专家修订原始策略草稿后重新提交，而非尝试在错误的骨架上修修补补。
这一框架的价值在于它重新定义了人机关系。它不追求用 AI 替代数学家，而是让 AI 成为数学家思维的 “外骨骼”—— 专门负责承重和执行那些标准化、技术性的展开工作，从而让人类得以从繁琐的细节中解放，将宝贵的脑力聚焦于更高层次的策略创新与概念突破。正如陶哲轩所总结的，这种方法特别适用于 “技术性强、概念性弱” 的证明环节。通过将协作锚定在 “策略草稿” 这一中间层，我们既避免了 AI 因缺乏高层理解而产生的 “幻觉”，也避免了人类因陷入细节泥潭而错失的灵感火花。未来，随着模型能力的提升，这一框架可以进一步扩展，例如让 Claude 在人类提供的多个策略草稿中进行初步评估和排序，但其核心 —— 人类主导策略、AI 辅助展开 —— 必须作为不可动摇的基石。唯有如此，我们才能真正驾驭 AI 的力量，共同探索数学那未知而壮丽的疆域。