陶哲轩最新视频实验引发AI圈热议，这次他用AI工具挑战在Lean证明系统中完成代数蕴含的自动形式化。Claude仅用20分钟就成功通关，而o4-mini却因过于谨慎选择弃赛。这场测试不仅展示了AI在数学证明中的潜力，更揭示了自动化工具在效率与正确性之间的微妙平衡。

这次测试围绕一个代数蕴含展开：证明方程1689蕴含方程2。在正式实验前，陶哲轩先进行了初步验证。他将非形式化证明、形式化证明和方程内容作为附件，直接粘贴到Claude和o4-mini的输入框中，观察这两个模型的表现。

模型表现对比

Claude在测试中展现出明显优势。它能迅速将非形式化证明的单行内容转化为结构合理的Lean代码，成功定义了关键的幂函数。然而在实际编译过程中，Claude出现了错误——它默认自然数从1开始，而Lean系统中的自然数是从0开始的。这导致部分逻辑推导出现偏差。

更值得注意的是，Claude未能正确处理方程的对称性问题。例如在x=(y·x)·z的等式中，它未能识别出变量间的对称关系，影响了证明的完整性。尽管单行代码生成效率高，但缺乏对整体结构的把握，使得错误诊断和修复变得困难。

通过人工干预，陶哲轩最终在20分钟内完成形式化。这表明尽管AI工具能快速生成代码，但在复杂逻辑处理上仍需人类介入。这种人机协作模式，恰是当前形式化数学证明的主流方式。

o4-mini的表现则显得更为谨慎。它在初始阶段就识别出幂函数定义中的问题，正确指出magmas中没有单位元1，因此不能简单假设0→x等于1。这种严谨性避免了严重错误，但也导致它在关键时刻选择放弃，仅生成部分证明代码。

当遇到修复步骤时，o4-mini输出了"抱歉"这样的表达，显示出其在复杂任务中的局限性。最终，它未能完成整个形式化证明。陶哲轩指出，这种谨慎策略虽然能避免错误，但在处理复杂任务时可能影响效率。

有趣的是，两个模型都遇到了相似的对称性问题，这表明当前LLM在处理数学逻辑时仍存在共同局限。这为AI工具在数学领域的应用提供了重要参考。

效率尺度分析

陶哲轩的实验揭示了形式化数学证明中效率的多维特性。他将效率划分为四个不同尺度：单形式化、单一引理形式化、单一证明形式化，以及「整个教科书」形式化。

在实际操作中，这些尺度的优化策略往往相互冲突。例如，依赖类型匹配工具canonical在「单行形式化」任务中表现出色，能快速解析并生成正确代码，几乎无需人工干预。但过度依赖这种工具会导致对证明整体结构的把握减弱。

当陶哲轩发现过度依赖canonical时，他逐渐失去了对证明步骤之间联系的理解。这使得在「引理形式化」任务中，诊断和修复错误变得更加困难。不过，这种手动检查过程反而加深了他对引理间关系的认识，提升了解决「单一证明形式化」任务的能力。

这种「意外收获」让陶哲轩意识到，完全依赖自动化工具可能会削弱人类对证明结构的洞察。这在更大尺度的数学形式化任务中尤为重要。他得出结论，最佳的自动化水平应介于0%和100%之间，既保留人工干预的空间，又发挥工具的效率优势。

在面对中等及高难度任务时，过度依赖单一尺度的效率优化可能会影响工具的可靠性。这提醒我们，数学形式化的终极目标不仅是生成可编译的代码，更是构建一个灵活、可用且不断演进的形式化数学体系。

这场实验不仅验证了AI在数学证明中的潜力，更揭示了人机协作在复杂任务中的重要性。通过合理利用自动化工具，人类可以更高效地完成形式化工作，同时保持对数学结构的深入理解。这种平衡的实现，正是当前AI在数学领域应用的关键。