北京
新智元报道
编辑：桃子
【新智元导读】陶哲轩YouTube视频第二弹震撼来袭！这一次，他让AI挑战在Lean中形式化代数蕴含证明，结果Claude约20分通关，o4-mini太过谨慎直接「弃赛」。
3天后，陶哲轩YouTube视频二更来了。
这次，他尝试了一种更短、更概念化的证明版本，并测试Claude、o4-mini能否基于之前的非形式和形式证明，生成类似的形式化代码。
实验的核心是，在Lean中形式化同一个代数蕴含的证明。
此外，他还发文深入剖析了，自动化工具不同尺度上的效率表现，以及自动化与人工干预之间的微妙平衡。
Claude 20分完成，o4-mini弃题
最新实验中，陶哲轩围绕一个代数蕴含展开（algebraic implication）：证明方程1689蕴含方程2。
录制前，他已进行了一次测试。
这里直接在Claude/o4-mini中粘贴prompt，然后附上非形式证明、形式证明、方程三个附件。
接下来，一起看看这两个模型具体表现如何？
Claude
实验中，Claude整体表现出色，能够快速将非形式证明的单行，转化为看似合理的Lean代码。
它生成了与之前形式化证明结构相似的代码，并成功定义了关键的幂函数。
然而，陶哲轩创建一个新文件，在Claude编译过程中，却发现错误——它假设从自然数1开始，而Lean中的自然数从0开始。
另外，Claude未能正确处理方程的对称性，比如x=(y·x)·z，导致了证明逻辑出现偏差。
尽管单行代码生成高效，但缺乏对整体结构的理解，使得错误诊断和修复变得困难。
通过人工干预，陶哲轩修复了这些问题，最终在20分钟内完成形式化。
o4-mini
相比之下，o4-mini表现得更为谨慎。
与Claude类似，o4-mini一上来也创建了一个幂函数，却胜过前者。
它正确识别了幂函数定义中的问题，magmas中没有单位元1，因此不能简单假设0=>x设置为等于1。
然而，o4-mini在关键时刻却选择了「放弃」，仅生成了部分证明代码，并在修复步骤中输出「抱歉」。
最终，o4-mini未能完成形式化证明。
陶哲轩表示，它的谨慎策略虽避免了严重错误，但也限制了其在复杂任务中的实用性。
有趣的是，o4-mini和Claude同样遇到了类似对称性问题，表明LLM在处理数学逻辑的细微差别时，存在共同的局限。
总之，整个实验目标看似简单，即让AI工具将人类可读的证明转化为Lean代码，并在证明助手中成功编译。
然而，陶哲轩的实验揭示了自动化的复杂性，尤其是在效率和正确性之间的平衡。
100%过度自动化，毁掉数学未来？
在长达一周的自动形式化实验中，陶哲轩得出了一个教训——
即使纯粹专注于效率，仅接受在证明助手中实际编译并产生预期结果的形式化，衡量效率的尺度现在也产生了显著差异。
在形式化数学证明过程中，效率可以从以下四个不同尺度衡量。
1. 单形式化：加快证明中任意一行的形式化
2. 单一引理形式化：加快形式化证明中的任一引理
3. 单一证明形式化：加快形式化定理的任一证明
4. 「整个教科书」形式化：加快形式化整个教科书的成果
每个尺度看似都在指向同一个目标：更快地完成形式化。然而，实际操作中，这些尺度的优化策略可能互相冲突。
陶哲轩以自己最近的实验为例，尝试用一些自动化工具，加速形式化过程。
我意识到，许多当前的自动化工具可以在其中一个尺度上加速形式化，但出乎意料的是，过度依赖此类工具可能会削弱在其他尺度上形式化的能力。
比如，依赖类型匹配工具canonical在「单行形式化」（尺度1）的任务中，表现出色。
它能快速解析，并生成正确的代码，在此过程中，陶哲轩几乎无需手动干预。
然而，当过于依赖canonical，盲目接受它对某一步的解析，并迅速进入下一步时，他发现自己逐渐失去了对证明整体结构的把握。
这导致了，在「引理形式化」（尺度2）上，诊断和修复错误变得更加困难，因为到了此刻，陶哲轩对证明步骤之间的联系缺乏深入的理解。
有趣的是，修复这些错误的过程，却让陶哲轩本人受益匪浅。
通过手动检查和调整，他逐渐理解了引理之间的作用，这反过来提升了其解决「单一证明形式化」（尺度3）任务的能力。
这种「意外收获」让他意识到，完全依赖自动化工具，可能会让自己错过对证明结构的深刻洞察，而这些这些洞察在更大尺度上至关重要。
陶哲轩认为结论是，「最优的自动化水平并不是100%，而是介于0%和100%之间的某个值」。
从每个尺度上来说，自动化工具应该被用来减少重复性的繁琐工作，但同时必须保留足够的人为干预，以审查和修复局部问题，从加深人类对所有尺度任务结构的理解。
更广义地看，如果我们100%依赖自动化工具解决所有任务，可能会失去对任务空间的熟悉度。
在面对中等，甚至高难度任务时，自动化工具可靠性下降，我们却可能因缺乏经验而束手无策。
值得警醒的是，过度聚焦于单一尺度的效率优化，可能会违背数学形式化的长远目标。
其终极目标，不仅是生成在证明助手中编译的代码，更是要创造一个灵活、可用、不断演变且富有启发性的形式化数学语料库。
参考资料：
https://mathstodon.xyz/@tao/114498906474280949
https://mathstodon.xyz/@tao/114501119350851281
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
