GitHub Copilot在数学定理证明中的应用 - 核心观点：GitHub Copilot在数学定理证明中主要起辅助作用，能快速生成代码框架和常见模式，但复杂数学细节和创造性解决方案仍需人工干预[5][6][7] - 陶哲轩演示了如何正确引导Copilot完成函数极限问题的求和、求差和求积定理证明[3][11][13][25][33] 具体证明过程 求和定理证明 - Copilot自动补全了ε-δ定义，但需手动调整绝对值符号表达[12] - 生成基本证明框架，但δ的正性验证和不等式处理不严谨，需人工修正绝对值符号、三角不等式应用和最终表达式[17][18][20] - 后期提示使用Lean内置的add_sub_add_comm引理简化步骤[23][24] 求差定理证明 - 沿用求和定理的框架，但虚构不存在的sub_sub_anc方法[27][28] - 处理代数表达式时不稳定，需手动完成恒等式证明[31][32] 求积定理证明 - 提出ε分配策略（ε/(2|M|+1)和ε/(2|L|+1)），但实现时出现正性验证和绝对值不等式错误[34][37][43] - 错误使用add_lt_add方法，需人工调整假设条件[37][39] - 建议复杂问题先用纸笔推导再形式化验证[41][42] Copilot的功能特点 - 优势：快速生成代码框架、提示库函数使用，对初学者友好[6][24] - 局限性：复杂数学细节可靠性低，易虚构方法或忽略适用条件[7][28][37][40]