在探索大语言模型（LLM）于形式化数学领域的应用时，Anthropic 的 Claude 模型因其强大的代码生成与结构模仿能力而备受关注。然而，真实世界的能力测绘，如数学家陶哲轩的最新实验所揭示的，并非一帆风顺。该实验要求 Claude 将一个代数蕴含的非形式化人类证明，转化为能在 Lean 证明助手中成功编译的形式化代码。Claude 虽在约 20 分钟内 “通关”，但其过程暴露了清晰的能力边界，为我们提供了宝贵的实战洞察：自动化工具的价值不在于取代人类，而在于如何与人类智慧高效协同。
Claude 在此类任务中的核心优势在于其 “单行形式化” 能力。它能迅速解析人类证明的单个步骤，并生成语法上看似合理、结构上与先前形式化证明高度相似的 Lean 代码片段。这种高效的 “翻译” 能力极大地加速了初始代码的骨架搭建，尤其是在定义关键函数（如实验中的幂函数）时，展现了其对模式识别的强大天赋。这使得开发者能从繁琐的、重复性的代码敲击中解放出来，将精力集中在更高层次的逻辑设计上。
然而，陶哲轩的实验清晰地划定了 Claude 的能力边界，主要体现在对数学基础公理和逻辑细微差别的处理上。其生成的代码在编译时暴露出两个典型错误：首先，它错误地假设 Lean 中的自然数从 1 开始，而实际上 Lean（以及大多数形式化系统）的自然数定义是从 0 开始。这一根本性错误源于模型对形式化系统底层公理的 “健忘” 或 “误解”，它未能将人类证明中的自然数概念与 Lean 的严格定义进行精确对齐。其次，Claude 在处理方程的对称性（如 x=(y・x)・z）时出现了逻辑偏差，未能正确推导出等价变换，导致证明链条断裂。这表明模型在进行多步骤、深层次的逻辑推理时，缺乏对整体结构的连贯性把握，容易陷入局部最优而忽略全局约束。
基于此，我们提炼出一份针对 Claude 形式化验证任务的 “可落地错误诊断清单与人工干预策略”，以最大化其效率并规避风险：
- 公理与定义核查清单：在 Claude 生成任何涉及基础数学对象（如自然数、整数、集合）的代码后，人工必须立即核查其定义是否与目标形式化系统（如 Lean, Coq）的公理完全一致。重点检查起始值、运算符定义和归纳原理。
- 对称性与等价性验证点：对于涉及方程变换、逻辑等价或对称操作的证明步骤，不应直接采纳 Claude 的输出。开发者应手动推导或使用形式化系统内置的定理库进行验证，确保每一步变换都严格成立。
- 结构审查与 “思考暂停” 策略：不要盲目接受 Claude 生成的连续代码块。应在每个关键引理或证明段落结束后，强制 “暂停”，由人工审查代码的整体逻辑流，理解各部分之间的依赖关系。这不仅能及时发现错误，更能加深开发者对证明结构的理解，为后续调试奠定基础。
- 渐进式自动化原则：遵循陶哲轩提出的 “最优自动化水平并非 100%” 的洞见。将 Claude 定位为 “高级助手” 而非 “全自动引擎”。用它来完成 80% 的机械性工作，但保留 20% 的关键决策和验证环节由人类掌控。这种混合模式能有效平衡效率与正确性，防止因过度依赖而导致的 “能力退化”—— 即开发者因缺乏深度参与而丧失诊断和修复复杂错误的能力。
总而言之，Claude 在形式化验证领域展现的是一种 “强大的辅助能力” 而非 “完全的自主能力”。其价值在于加速过程，但其局限性要求我们必须保持清醒的人工干预。通过实施上述诊断清单与干预策略，我们可以将 Claude 的潜力转化为可靠的形式化生产力，共同推动人机协作在严谨数学领域的边界。