机器之心报道
编辑：大盘鸡
AI 将大大提高数学研究的效率。
陶哲轩是公认的数学天才，被誉为「数学神童」。他从小便展现出惊人的数学天赋，9 岁时就参加了美国数学奥林匹克，并获得了金牌。他在数论、调和分析、偏微分方程等多个数学领域做出了重要贡献，并获得了菲尔兹奖， 这一奖项被视为数学界的最高荣誉，相当于数学界的诺贝尔奖。
最近，陶哲轩接受了《科学美国人》的采访。在采访中提出，未来数学家可以通过向类似 GPT 的 AI 解释证明，AI 会将其形式化为 Lean 证明。这种助手型 AI 不仅能生成 LaTeX 文件，还能帮助提交论文，从而大幅提高数学家的工作效率和便利性。
他强调，AI 和自动化证明检查器的引入将使得数学领域的合作方式发生根本性变化。通过将证明分解成小部分并由计算机验证，数学家们可以在更大规模的项目上合作，而无需逐一验证每个人的工作。
采访文章地址：https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/
不过，这个讨论也引起了一些争议。有人认为这会导致数学家变得懒惰和粗心，还可能导致数学证明的严谨性和创造力的下降。然而，陶哲轩解释说，这种技术实际上是为了减轻数学家在证明过程中的繁琐工作，让他们可以专注于更具创造性和复杂性的任务
尽管陶哲轩对 AI 在数学中的应用持乐观态度，他也承认当前技术尚未完全准备好。目前的 AI 在处理数学家直觉和知识的方面还存在局限，很多数学知识并未在已发表的论文中捕获，而是在对话和讲座中传授。
陶哲轩提供了一个复杂分析问题的示例，他通过与 ChatGPT 互动，解释问题并生成了一个 LaTeX 文件。虽然目前的技术尚未实现完全形式化验证，但这一示例展示了 AI 在协助数学证明方面的潜力。
陶哲轩昨日在博客中，对自己在采访中的观点进行了进一步解释。
他谈到自己在《科学美国人》中谈到的观点：我认为在未来，我们将不再需要手动输入证明，而是将它们讲解给某种 GPT。这个 GPT 会在你讲解的过程中尝试将其形式化为 Lean 语言。如果一切都检查无误，GPT 会说：这是你的 LaTeX 数学论文；这是你的 Lean 证明，如果你愿意，我可以按下这个按钮并将其提交给期刊。它将成为一个非常棒的助手。
这句话似乎引起了不同的反响，特别是被解读为数学家会变得懒惰和草率。我认为最好的方式来说明我的观点是通过一个实际示例，这已经是现有技术可以实现的。在我有一个中等难度的复分析问题。我在解释了这个问题及其解决方案后，GPT 能够提供解决方案的 LaTeX 文件。GPT 表现得相当不错，将我草拟的论证扩展为一个相当连贯且相对严谨的完整证明。这还不是我在文章中设想的 100%，特别是缺少了保证正确性的严格 Lean 转换，但希望能说明我在这句话中的想法。
陶哲轩还补充说道， 采访中提及按下按钮将 GPT 生成的 LaTeX 文章提交给期刊的部分带有玩笑性质。但他认为未来期刊会制定过滤器、标签要求和其他规则来管理部分或全部由 AI 生成的投稿。同时，他设想了新的文化规范，例如将 AI 生成并与 Lean 集成的互动形式的论文作为辅助版本，而人类撰写的文本仍作为主要权威版本。
也有网友表示，最大的难题其实是验证证明的正确性。陶哲轩对此回应道：
我认为，采用新的工作流程实践（例如那些在软件工程或现有的形式化项目中已成为标准的流程）可以解决其中的许多问题。例如，应该在开始证明过程之前先形式化结果的陈述，而不是在之后。我们还可以半自动或自动地对陈述进行各种「合理性检查 」或 「单元测试」，例如测试定理的琐碎或非常简单的情况，以及已知的更强版本定理的反例。(例如，在我的例子中，我加入了对该定理反例的验证作为一种合理性检查，尽管实际上目标并不需要它）。
可见 AI 在数学领域的潜力巨大。在 AI 技术的辅助下，数学家的角色也将变得更加多样化。未来可能出现的角色包括项目经理、专门的 AI 培训师，以及将 AI 生成的证明转化为人类可读形式的专家。这将使数学研究更加类似于现代工业中的分工合作模式 。
如陶哲轩所说， AI 技术不仅能提高数学家的工作效率，还能通过形式化验证保证证明的准确性。这将为数学研究带来革命性的变化，促使数学家在更短的时间内取得更大的成果 。
参考链接：
https://mathstodon.xyz/@tao
https://www.scientificamerican.com/article/ai-will-become-mathematicians-co-pilot/
© THE END