AI将是数学家的得力助手，陶哲轩谈AI在证明过程中的潜力

陶哲轩，一位公认的数学天才，曾在9岁时参加美国数学奥林匹克并获金牌，在数论、调和分析、偏微分方程等领域做出重要贡献，并获得菲尔兹奖。他最近在接受《科学美国人》采访时提出，未来数学家可以通过向类似GPT的AI解释证明，AI会将其形式化为Lean证明，从而大幅提高数学家的工作效率和便利性。他强调，AI和自动化证明检查器的引入将使得数学领域的合作方式发生根本性变化。虽然有人担心这会导致数学家变得懒惰和粗心，陶哲轩解释说，这种技术实际上是为了减轻数学家在证明过程中的繁琐工作，让他们可以专注于更具创造性和复杂性的任务。他也承认当前技术尚未完全准备好，很多数学知识并未在已发表的论文中捕获，而是在对话和讲座中传授。他认为，采用新的工作流程实践可以解决验证证明正确性的问题。AI在数学领域的潜力巨大，未来可能出现的角色包括项目经理、专门的AI培训师，以及将AI生成的证明转化为人类可读形式的专家。这将使数学研究更加类似于现代工业中的分工合作模式。