人机协作新范式：让Claude生成可验证的数学证明策略草稿

在数学形式化证明的浪潮中，一个关键却被忽视的环节正浮出水面：策略草稿的生成。当前多数讨论聚焦于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的力量，共同探索数学那未知而壮丽的疆域。