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/