陶哲轩的YouTube视频第二弹重磅上线！此次，他让AI在Lean系统中挑战形式化代数蕴含的证明，Claude在约20分钟内完成，而o4-mini则因过于谨慎而选择“放弃比赛”。

仅仅三天后，陶哲轩在YouTube上发布了视频的更新。

上次，他利用GitHub Copilot（基于GPT-4技术），在33分钟内成功完成了一页的非形式化证明。

这一次，他探索了一种更短且概念化的证明方式，并检验Claude和o4-mini能否基于之前的非形式与形式证明，生成相应的形式化代码。

该实验的核心在于，在Lean中对同一代数蕴含的证明进行形式化处理。

此外，他还深入分析了不同规模自动化工具的效率表现，以及自动化与人工干预之间的微妙平衡。

Claude 20分钟完成，o4-mini选择放弃

在最新的实验中，陶哲轩围绕一个代数蕴含展开（algebraic implication）：证明方程1689包含方程2。

在录制之前，他已经进行了一次测试。

他在Claude和o4-mini中直接粘贴了提示，并附上了非形式证明、形式证明及方程的三个附件。

接下来，我们一同来看看这两个模型的具体表现如何。

Claude

在实验过程中，Claude展现了出色的表现，能够迅速将非形式证明的单行转化为看似合理的Lean代码。

它生成了与之前形式化证明结构相似的代码，并成功定义了关键的幂函数。

然而，在陶哲轩新建文件并进行Claude编译时，他发现了一个错误——Claude假设自然数是从1开始，而Lean中的自然数是从0开始。

此外，Claude在处理方程的对称性时出现了问题，例如x=(y·x)·z，这导致了证明过程中的逻辑偏差。

尽管生成的单行代码效率极高，但其对整体结构的理解不足，使得问题的诊断与修复变得异常困难。

经过人工干预，陶哲轩解决了这些问题，并最终在20分钟内完成了形式化的过程。

o4-mini

与此相比，o4-mini的表现则显得更加谨慎。

o4-mini与Claude相似，首先也创建了一个幂函数，但在许多方面超越了前者。

它能够准确识别幂函数定义中的问题，意识到在magmas中并不存在单位元1，因此不能简单地假定0=>x等于1。

然而，o4-mini在关键时刻选择了「放弃」，仅生成了部分证明代码，并在修复过程中表示「抱歉」。

最终，o4-mini未能成功完成形式化证明的任务。

陶哲轩评论说，虽然它的谨慎策略防止了重大错误，但在复杂任务中却也显得不够实用。

有趣的是，o4-mini与Claude一样都面临对称性问题，这表明大型语言模型在数学逻辑的微妙差异处理上存在共通的局限性。

综上所述，这一实验的目标看似简单，即让AI工具将人类可读的证明转换为Lean代码，并在证明助手中成功编译。

然而，陶哲轩的实验揭示了自动化过程中的复杂性，尤其是在效率与正确性之间的微妙平衡。

100%过度自动化，是否会毁掉数学的未来？

在为期一周的自动形式化实验中，陶哲轩得出了一个重要的教训——

即使在专注于效率时，仅仅依赖于在证明助手中实际编译并产生预期结果的形式化，其衡量效率的标准现在也存在显著差异。

在进行形式化数学证明的过程中，效率可以从以下四个不同的维度来评估。

1. 单行形式化：提升证明中任意一行的形式化速度

2. 单一引理形式化：加速任一引理的形式化过程

3. 单一证明形式化：加快任一定理的形式化证明

4. 「整本教科书」形式化：加快形式化整本教科书的进程

虽然每个维度看似都指向同一目标，即更快的完成形式化，但在实际操作中，这些维度的优化策略可能会产生相互冲突的情况。

陶哲轩最近在实验中探讨利用一些自动化工具来加速形式化的进程。

他意识到，虽然现有的自动化工具在某些方面能够提升形式化速度，但令人意外的是，过于依赖这些工具可能会削弱在其他方面的形式化能力。

例如，类型匹配工具canonical在“单行形式化”（尺度1）任务中表现优异。

它能够迅速解析并生成正确的代码，在此过程中，陶哲轩几乎不需要进行手动干预。

然而，当他过于依赖canonical，盲目采纳它对某一步骤的解析，并迅速推进至下一步时，逐渐发现自己对整体证明结构的把握越来越薄弱。

这种情况导致在“引理形式化”（尺度2）中，错误的诊断和修复变得更加复杂，因为此时陶哲轩对证明步骤之间的联系缺乏深入的理解。

有趣的是，修复这些错误的过程却为陶哲轩带来了意想不到的好处。

通过手动检查和调整，他逐渐理解了引理之间的关系，这反过来又增强了他解决“单一证明形式化”（尺度3）任务的能力。

这种“意外收获”让他认识到，完全依赖自动化工具可能会使人失去对证明结构的深刻洞察，而这些洞察在更广泛的范畴中至关重要。

陶哲轩总结道，“理想的自动化水平并非100%，而是介于0%与100%之间的某个值”。

从每个尺度来看，自动化工具应当用于减少重复性繁琐的工作，但同时也需要保留足够的人为干预，以便审查和修复局部问题，从而加深人类对各个尺度任务结构的理解。

更广泛地说，如果我们完全依赖自动化工具来完成所有任务，可能会失去对任务空间的熟悉感。

在面对中等甚至高难度的任务时，自动化工具的可靠性可能下降，而我们可能因为缺乏经验而陷入困境。

值得注意的是，过于关注单一尺度的效率优化，可能会背离数学形式化的长远目标。

最终目标不仅是生成在证明助手中可以编译的代码，更是创造一个灵活、可用、不断演变并富有启发性的形式化数学语料库。

参考资料：

https://mathstodon.xyz/@tao/114498906474280949

https://mathstodon.xyz/@tao/114501119350851281

本文由微信公众号“新智元”提供，作者：新智元，36氪经授权发布。