共计 2502 个字符，预计需要花费 7 分钟才能阅读完成。
陶哲轩的YouTube视频第二弹引发热议！这一回，他让AI挑战在Lean中进行代数蕴含的形式化证明，结果Claude在约20分钟内顺利完成，而o4-mini则因为过于谨慎选择了“弃赛”。
仅过3天，陶哲轩便发布了YouTube视频的更新。
在之前的实验中，他利用GitHub Copilot（基于GPT-4技术），在短短33分钟内完成了一页非形式化证明。
此次，他尝试了一种更为精简且概念化的证明模式，并检验Claude和o4-mini能否基于之前的非形式与形式证明，生成类似的形式化代码。
实验的重点是，在Lean中对同一代数蕴含的证明进行形式化处理。
此外，他发布了一篇文章，深入分析了自动化工具在不同层次上的效率表现，以及自动化与人类干预之间的微妙平衡。
Claude在20分钟内完成，o4-mini选择放弃
在最新的实验中，陶哲轩专注于一个代数蕴含问题：证明方程1689是否蕴含方程2。
录制之前，他已经进行了初步测试。
此时，他在Claude和o4-mini中直接粘贴了提示，并附加了非形式证明、形式证明和方程三个文件。
接下来，让我们一起探讨这两个模型的具体表现。
Claude的表现
在实验中，Claude展现了令人印象深刻的能力，能够迅速将非形式证明的单行转化为看起来合理的Lean代码。
它生成了与之前形式化证明结构相似的代码，并成功定义了关键的幂函数。
然而，陶哲轩在创建新文件并编译Claude时，却发现了一个错误——Claude假设自然数从1开始，而在Lean中，自然数是从0开始的。
参考文章： 液晶电视屏幕出现竖条纹的原因及解决方法解析
AI在数学证明中的挑战与机遇
在陶哲轩的实验中，Claude在处理方程的对称性时出现了问题，例如在表达式x=(y·x)·z中，导致证明过程中逻辑的偏差。
虽然单行代码的生成效率较高，但由于缺乏对整体逻辑结构的把握，使得错误的识别与修复变得异常艰难。
经过人工干预，陶哲轩成功解决了这些问题，并在短短20分钟内完成了形式化的过程。
o4-mini的谨慎策略
与Claude相比，o4-mini展现出更加谨慎的态度。
它在一开始便创建了一个幂函数，表现上超过了前者，准确地识别了幂函数定义中存在的问题。尤其是在magmas中没有单位元1的情况下，不能轻易假设0=>x等于1。
然而在关键时刻，o4-mini却选择了部分放弃，仅生成了有限的证明代码，并在修复步骤中输出了「抱歉」的提示。
最终，它未能完成形式化证明。陶哲轩指出，这种谨慎策略虽然有效避免了重大错误，但在复杂任务中的实用性却受到限制。
值得注意的是，o4-mini与Claude同样遭遇了对称性的问题，显示出大型语言模型在处理数学逻辑的细微差别时的共同局限。
总而言之，这项实验的目标是让人工智能工具将人类可读的证明转化为Lean代码，并在证明助手中成功编译。
然而，陶哲轩的探索揭示了自动化过程中面临的复杂性，尤其是在效率与准确性之间的权衡。
过度依赖自动化，是否会影响数学的未来？
在为期一周的自动形式化实验中，陶哲轩领悟到一个重要的教训——
即使专注于效率，只有在证明助手中实际编译并获得预期结果的形式化，其衡量效率的标准也显著不同。
在形式化数学证明的过程中，效率可以从以下四个不同的维度进行衡量：
1. 单行形式化：加速证明中任意一行的形式化处理。
2. 单一引理形式化：提升形式化证明中任意引理的速度。
3. 单一证明形式化：加快形式化定理的某一证明过程。
4. 整个教科书形式化：加速形式化整个教科书的成果。
表面上看，这些尺度都指向同一个目标：更高效地完成形式化。然而，在实际操作中，优化策略之间可能会产生相互冲突的情况。
陶哲轩在最近的实验中，展示了如何利用一些自动化工具来加速数学形式化的进程。
他发现，尽管目前的许多自动化工具能够在某一特定尺度上提升形式化的效率，然而，过度依赖这些工具可能会削弱在其他尺度上的形式化能力，令人意外。
例如，在处理“单行形式化”（尺度1）时，类型匹配工具canonical表现尤为出色。
该工具能够迅速解析并生成正确代码，陶哲轩几乎不需要手动干预。
但如果过于依赖canonical，并盲目接受其解析结果，迅速进入下一步骤，他却发现对证明整体结构的掌控逐渐减弱。
这种状况导致在“引理形式化”（尺度2）时，诊断和修复错误变得异常困难，因为此时陶哲轩对各证明步骤间的联系缺乏深入的理解。
有趣的是，这一修复过程却使陶哲轩获得了意想不到的收益。
通过手动检查和调整，他逐渐领悟了引理之间的相互作用，这也反过来增强了他在“单一证明形式化”（尺度3）任务中的能力。
这一“意外收获”让他意识到，完全依赖自动化工具可能会使他错失对证明结构的深刻理解，而这种理解在更大范围内至关重要。
陶哲轩总结道，最佳的自动化水平并非100%，而是介于0%与100%之间的某个值。
从每个尺度来看，自动化工具应当用于减少重复性工作，但同时也必须保留足够的人为干预，以便审查和修复局部问题，从而加深对各尺度任务结构的理解。
更广泛地说，若完全依赖自动化工具处理所有任务，我们可能会失去对任务空间的熟悉感。
在面对中等甚至高难度的任务时，自动化工具的可靠性可能会降低，而我们却可能因缺乏经验而陷入困境。
值得注意的是，过于专注于单一尺度的效率提升，可能会与数学形式化的长远目标背道而驰。
最终的目标不仅是生成可在证明助手中编译的代码，更是要创造一个灵活、实用、不断演变且富有启发性的数学形式化语料库。
参考资料：
https://mathstodon.xyz/@tao/114498906474280949
https://mathstodon.xyz/@tao/114501119350851281
本文由微信公众号“新智元”提供，作者：新智元，经36氪授权发布。
