技术博客

数学大师陶哲轩尝试与人工智能GitHub Copilot合作，利用Lean 4探索ε-δ极限问题的自动化证明。在加法定理的证明中，Copilot表现出色，但在减法和乘法部分遇到困难，尤其乘法几乎失控。这引发了关于AI是辅助工具还是干扰因素的讨论。