陶哲轩联合AI挑战经典ε-δ极限，加法秒杀，乘法翻车

第三支Leann大师陶哲轩 4自动数学证明视频来了！他与GitHub携手 Copilot挑战分析经典「ε-δ」极限问题:加法定律Copilot可以自由挥洒，减法开始卡住，乘法完全失控。Copilot是上帝的助攻还是混乱？

陶哲轩数学大师的AI新试验来了！

这次Lean 四是自动数学证书的第三个视频。

主要看GitHub 处理分析经典的Copilot「ε-δ」当问题(描述函数极限的经典方法)出现时，效果如何？

此前，陶哲轩上传了两个这一系列视频。

此外，此次共有3个视频，陶哲轩的油管频道已有17,000名订阅者。

看起来，他作为菲尔兹获得者，是当代最杰出的数学家之一，其影响的确是毋庸置疑的。

在这次定律形式化演示中，陶哲轩发现，GitHub 在帮助初学者和处理基础任务之后，Copilot表现得相当不错。

它可以帮助用户快速介绍Lean语言(一种交互式定理证明工具)，提供语法提醒，并且可以智能地补充基本的定义和说明。

Copilot可以准确地预测结构和关键步骤，例如函数极限和定律中的结构和关键步骤，表现为左膀右臂。

但是当证实复杂性时，Copilot的缺点就暴露出来了。

比如在处理函数极限的差异和积定律时，在复杂的代数推导、寻找合适的数学引理(如与平方根相关的引理)等方面显得无能为力。

有时候Copilot也会出现「幻觉」，生成一种完全不存在的策略，或犯一些低级错误，导致证明过程混乱。

此时，陶哲轩不得不亲自出马，纠正错误，甚至完全接管证实。

「人机协作」的证明过程

形式化数学的目的是用计算机能够完全理解的准确语言，一步一步地检查推理是否可靠，然后写出数学的概念和确认，然后使用定理证明工具(比如视频中提到的Lean)。

它就像把数学证书翻译成一种特别严格的编程语言。

在第三弹视频中，陶哲轩从一个经典的分析概念开始：函数的极限。

对于初学者小白来说，用Lean写出这个定义并不容易。但是，GitHub Copilot就像一个贴心的助手，派上了很大的用场。

陶哲轩刚刚敲下来「定义一个谓词limit f x₀ l」，Copilot立刻得到了他想要表达的东西。「ε-δ」极限定义，每秒生成相应的Lean代码。

虽然陶哲轩根据自己的习惯稍作调整，但是Copilot的智能化补充显然使整个过程更加迅速。

「和的极限」——小试牛刀

下一步，陶哲轩挑战了一个更复杂的定律：如果函数f(x)极限为L，g(x)极限是M，那么f(x) g(x)极限就是L M。

Copilot又展示了一个操作。这不仅帮助陶哲轩描述了定律的Lean声明，而且开始「猜」确认过程，建议引入假设，提取出来ε和δ这是关键变量。

Copilot试图使用Lean的calc块来整理不等式链，并且试图使用simp来简化关系。

但是在这里，它开始犯小错误，比如弄乱了绝对值的位置，或者在代数推导中看起来不够。「机智」。

比如，陶哲轩不得不出手，他提醒Copilot使用。「ε/2」技巧。尽管Copilot一开始并没有完全跟上，但是经过调整，它已经成功地融入了这个想法。

最终，经过一番人机配合，这个「和的极限」在Lean中，定律得到了成功的证实。

陶哲轩认为，Copilot做了大部分的工作，互动体验也很好。

「差的极限」——AI有点懵

有了「和的极限」陶哲轩认为的经历「差的极限」同样顺利。这一定律意味着如果f，(x)极限为L，g(x)极限是M，那么f(x)-g(x)的极限是L-M。

Copilot似乎也充满了信心，直接应用。「和的极限」证明招数，甚至使用上面提到的「ε/2」的技巧。

但是在这个过程中，Copilot仍然卡住了，「脑补」一种在Lean中根本不存在的策略(叫什么subb？ subanc）。

面临Copilot「胡思乱想」，陶哲轩试图提醒他，但是Copilot仍然不明白。

陶哲轩意识到，这些代数转换对人类来说很简单，但需要调用特定的数学引理来支持Lean中的每一步。最后，陶哲轩只能自己完成这些代数推导。

这个关卡让陶哲轩看到，Copilot虽然可以模仿证明的大框架，但是在需要特定的引理或者复杂的代数操作时，很容易掉链子。

对于Copilot这一关的表现，他打了一个B ：我帮了很多忙，但在关键时刻，我还是要依靠人类的引导甚至接管。。

「积的极限」——完全乱套

最难的来了：如果f(x)极限为L，g(x)极限是M，那么f(x)·g(x)的极限是L·M。

这一确认比加减法复杂得多，特别是控制偏差。（ε）时间，堪称噩梦。

试着沿用Copilot的标准招数，加上中间项、三角形不等式。

但是问题来了，Lean需要一个非常具体的引理来处理平方根的乘法或者求和，比如把|ab|变成|a||b|用abs_mul，|a b|≤|a| |b|使用abs__add。

Copilot在寻找这些引理时经常出错，甚至想使用一些通用的策略(比如线性算术)，但由于乘法和平方根，它们行不通。

更加麻烦的是，为了使误差得到控制。ε在内部，一开始要精心策划f。(x)和g(x)误差参数。对于Copilot来说，这些参数的选择和界限估计有点太难了。它尝试了一些参数，但在确认中发现它不起作用，甚至差点出现除以零的错误。

在这个阶段，陶哲轩花了很多时间「灭火」，不断优化Copilot的尝试，寻找正确的引理，甚至回去改变最初的偏差参数。

整个过程是混乱的。虽然Lean系统更改参数相对方便(只需要更改系统进行重新检查)，但在知道如何更改之前，必须对确认结构有一个清晰的认识。

最终，陶哲轩经过艰苦的努力和大量的人工控制，完成了。「积的极限」证实。

他总结说，Copilot一旦被证明复杂到一定程度，就会变得复杂。「不太可靠」了。

有意思的是，大多数观众认为视频做得很好，但很多网友建议陶哲轩换一个新的麦克风，以消除回声。

AI只是副驾驶

影片结尾，陶哲轩总结道：在证明过程复杂化的情况下，最好回到最传统的。「人脑」方法-用笔在纸上清楚地理解确认的思路和关键步骤，然后一步一步地确认器内的正式化。。

Copilot更像是你的。「左膀右臂」，适用于帮助您快速完成那些重复、格式化的工作，当您对方向有了大致的了解。

这是一个非常强大的辅助工具，但是确认的策略、方向和最终验证，仍然要靠人类自己来控制。

参考资料：

https://www.youtube.com/watch?v=XMtmfS81ix

本文来自微信微信官方账号“新智元”，作者：犀牛，36氪经授权发布。

本文仅代表作者观点，版权归原创者所有，如需转载请在文中注明来源及作者名字。

免责声明：本文系转载编辑文章，仅作分享之用。如分享内容、图片侵犯到您的版权或非授权发布，请及时与我们联系进行审核处理或删除，您可以发送材料至邮箱：service@tojoy.com