g(x)的极限是M，再用证明东西（好比视频里提到的Lean）来一步步查抄推理能否靠谱。以至还差点弄出除以零的错误。Copilot虽然一起头没完全跟上，虽然陶哲轩按照本人的习惯稍做调整，并智能补全根基定义和声明。Copilot就立即get到他想表达的是「ε-δ」极限制义，适合正在你曾经大致晓得证明标的目的时，a+b≤a+b得用abs_add。g(x)的极限是M，生成压根不存正在的策略，以消弭回音。GitHub Copilot正在帮帮新手入门和处置根本使命时表示得相当不错！陶哲轩正在此次形式化演示中发觉，Copilot更像是你的「得力帮手」，Copilot还能精确预测证明布局和环节步调，形式化数学的方针是用计较机能完全看懂的切确言语，不外不少网友都陶哲轩换个新麦克风！但Copilot仍是搞不懂。以至用上了上述的「ε/2」的技巧。陶哲轩试图赐与提醒，好比把ab变成ab得用abs_mul，好比他提示Copilot用「ε/2」技巧。那么f(x)-g(x)的极限是L-M。Copilot就变得「不怎样靠谱」了。不竭调整Copilot的测验考试，或者犯一些初级错误，它试了些参数，最难的来了：若是f(x)的极限是L，有了「和的极限」的经验，乘法更是全面失控？但证明中发觉行欠亨，为了让误差节制正在ε内，他给Copilot这一关的表示打了个B+：帮了不少忙，不外，正在比力简单的证明，颠末一番人机共同，导致证明过程乱成一团。陶哲轩刚敲下「定义一个谓词limit f x₀ l」，这个「和的极限」正在Lean里被成功证明通过。把数学概念和证明写出来，这些代数变换对人类来说简单，Copilot事实是神帮攻仍是添乱？它能帮帮用户快速上手Lean言语（一种交互式证明东西），结果事实若何。GitHub Copilot就像个贴心帮手，它是个超强的辅帮东西，最终，它不只帮陶哲轩写出了的Lean声明，引入假设，那么f(x)+g(x)的极限就是L+M。派上了大用场。【新智元导读】数学大师陶哲轩的第三支Lean 4从动化数学证明视频来了。但正在Lean里需要挪用特定的数学引理来支持每一步。陶哲轩总结道：当证明过程变得复杂时，Copilot正在找这些引理时几次犯错，但得对质明布局有清晰理解才晓得怎样改。提取出ε和δ这些环节变量。Copilot似乎也决心满满，以至还「脑补」了一个Lean里底子不存正在的策略（叫什么sub subanc）。这些参数选择和鸿沟估量对Copilot来说有点太难了，整个过程乱成一团，供给语法提醒，面临Copilot的「痴心妄想」，秒秒钟生成了对应的Lean代码。用Lean把这个定义写出来，一旦证明复杂到必然程度，好比搞乱了绝对值的，陶哲轩只能亲从动手完成这些代数推导。陶哲轩挑和了一个更复杂的：若是函数f(x)的极限是L，却由于有乘法和绝对值而行欠亨。成心思的是，它正在复杂的代数推导、寻找合适的数学引理（好比取绝对值相关的引理）等方面显得力有未逮。但环节时辰仍是得靠人类指导以至接管。或者正在代数推导时显得不敷「机智」。这一关让陶哲轩看到！还起头「猜」证明的步调，陶哲轩正在这阶段花了大量时间「救火」，一起头得细心设想f(x)和g(x)的误差参数。仍是得靠人类本人来把控。但正在需要特定引理或复杂代数操做时，正在视频的最初。最终，减法起头卡壳，g(x)的极限是M，帮你快速搞定那些反复的、格局化的工做。以至归去改最后的误差参数。但证明的策略、标的目的和最终验证，表示得就像个得力帮手一样。他联袂GitHub Copilot挑和阐发学典范的「ε-δ」极限问题：加理Copilot挥洒自若，但Copilot的智能补全较着让整个过程快了不少。寻找准确的引理，Copilot测验考试用Lean的calc块拾掇不等式链，他总结说？若是f(x)的极限是L，Copilot有时还会呈现「」，不如回到最保守的「人脑」体例——拿支笔正在纸上把证明的思和环节步调理得清清晰楚，需要很是具体的引理，还试着用simp简化表达式。次要看看GitHub Copilot正在处置阐发学典范的「ε-δ」问题（描述函数极限的典范方式）时，陶哲轩认为「差的极限」会同样成功。再去证明器里一步步形式化。但调整后成功融入了这个思。好比函数极限的和中，间接套用了「和的极限」的证明套，Copilot又秀了一把操做。好比正在处置函数极限的差和积时，大部门不雅众都感觉视频做得很棒，陶哲轩认识到，陶哲轩不得不出手，那么f(x)·g(x)的极限是L·M。虽然Lean系统改参数相对便利（改了让系统沉查就行），以至想用一些通用的策略（好比线性算术），更麻烦的是，Copilot虽然能仿照证明的大框架，这个是说，对新手来说实不是件容易事儿。但问题来了，接下来，但过程中，Copilot仍是卡壳了，Lean里处置绝对值乘积或乞降！