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

72 0 0

文章摘要

数学大师陶哲轩在第三支Lean 4自动化数学证明视频中，展示了GitHub Copilot在处理经典分析学问题「ε-δ」极限时的表现。视频中，陶哲轩通过Lean语言进行形式化数学证明，探讨了Copilot在不同复杂程度证明中的表现。Copilot在基础任务和简单证明中表现出色，能够快速生成代码并提供语法提示，但在复杂证明中则显得力不从心。

在「和的极限」定理中，Copilot能够准确预测证明结构并生成关键步骤，尽管在代数推导中出现了一些小错误，但经过陶哲轩的调整后，证明顺利完成。陶哲轩认为，Copilot在这一过程中起到了得力助手的作用，互动体验良好。然而，在处理「差的极限」时，Copilot的表现开始出现明显问题，尤其是在需要特定引理或复杂代数操作时，Copilot频繁出错，甚至生成了不存在的策略。陶哲轩不得不亲自接管证明过程，最终完成了定理的证明。

最复杂的「积的极限」证明则彻底暴露了Copilot的短板。在处理绝对值乘积和误差控制时，Copilot频繁出错，甚至差点导致除以零的错误。陶哲轩在这一过程中花费了大量时间进行调整和修正，最终通过人工干预完成了证明。他总结道，Copilot在复杂证明中变得「不怎么靠谱」，尤其是在需要特定引理和复杂代数操作时，Copilot的表现远不如人类。

陶哲轩在视频最后总结道，Copilot更像是一个「得力助手」，适合在已知证明方向时帮助完成重复和格式化的工作。然而，证明的策略、方向和最终验证仍需依赖人类的判断和把控。他建议，在复杂证明中，传统的「人脑」方式仍然是不可或缺的，Copilot则可以作为辅助工具，帮助提高效率。