技术博客

数学大师陶哲轩与AI工具GitHub Copilot合作，利用Lean 4探索ε-δ极限问题的自动化证明。在加法定理的证明中，Copilot表现出色，但在减法和乘法证明中逐渐失控，尤其在乘法部分几乎无法提供有效帮助。这一现象引发了对AI在数学证明中作用的思考：它是辅助工具还是可能增加复杂性？