“那些毕生钻研的天才又算什么？”……3小时涌现722篇论文，令人震惊与恐惧[读懂科学]
OpenAI公开372项研究成果……部分撤回、修正引发验证争议
韩国数学家们 "不应止于证明，还应带来新的洞见"
随着人工智能解决数学长期难题的研究成果接连涌现，全球数学界为之震动。
代数、几何、微分方程等多个领域共有722篇论文公开，其中包括一些数学家数十年来未能解决的问题的解法。然而，部分结果被撤回或修订，人工智能创造的数学成果究竟能在多大程度上得到认可，也因此引发争议。
电影《心灵捕手》（1997）中的一个场景。拥有天才般数学天赋的主人公 Will Hunting（Matt Damon）正在大学走廊的黑板上解数学题。电影《心灵捕手》剧照。
View original image人工智能一举发布722篇论文……数学界为何震惊
当地时间10月6日，OpenAI公开了利用大型语言模型生成的722篇数学论文。这些论文归为372项研究成果，涉及代数、几何、微分方程等多个数学领域。论文及相关资料发布在在线代码与研究资料共享平台GitHub上，供任何人查阅和验证。据OpenAI介绍，得出一项研究成果所投入的计算量，相当于让最先进的人工智能模型运行约3小时。
此次发布备受关注，是因为人工智能不再只是辅助解决已有数学问题，而是提出了新的证明和算法。据悉，其中还包括证明长期猜想不成立的反例，以及新的解决方法。不过，这些主张是否准确、具有怎样的学术价值，仍有待数学家进一步验证。
基础科学研究院离散数学组首席研究员 Eom Sangil 表示：“有的成果声称解决了著名的长期难题，有的提出了长期猜想的反例，还有的提出了令人难以想象的新算法，因此许多数学家似乎都感到惊讶。”
韩国科学技术院人工智能数学研究生院院长、数学科学系教授 Baek Hyeongryeol 也表示：“此次发布的成果中，有好几项涉及我研究领域内足以获得菲尔兹奖级别的问题。如果主要成果得到验证，数学界受到的冲击将非常大。”
证明出来并非终点……人工智能时代数学家的角色
问题在于验证。OpenAI公开的资料中包含可通过计算机核验数学证明的Lean格式证明，但并非所有论文都经过了这类验证。Lean是一款用于确认数学命题是否依照逻辑规则得到证明的程序。
Eom Sangil 指出：“此次公开的论文中，约42%附有Lean形式化证明，不到一半。其余论文只有文本，因此不能排除其中存在错误的可能。”事实上，截至10月8日14时20分，OpenAI表示已撤回公开成果中的3项，并修订、补充了十余项证明。
通过计算机验证也不意味着所有问题都迎刃而解。Eom Sangil 解释说：“Lean所能保证的，仅仅是一个可由Lean读取的命题已经得到证明。该命题是否与论文中的主张一致，仍须由人来阅读确认。”
OpenAI利用人工智能生成的数学论文及相关证明材料的GitHub代码库页面。部分论文还包含“Lean”格式的证明材料，可通过计算机验证数学证明的逻辑有效性。GitHub页面截图。
View original image论文的完成度以及对既有研究的贡献，也成为争议焦点。Baek Hyeongryeol 院长表示：“我读过的稿件读起来很困难。有不少地方先使用未经定义的术语，过了很久才给出定义，读者不得不前后翻阅才能确认含义。”他还指出：“论证整体采用了什么结构、核心思路是什么，也没有清晰呈现。”
对于人工智能只是解决了既有研究最后一步的评价，他持谨慎态度。Baek Hyeongryeol 院长强调：“在数学中，最后一步也可能是最难的。重要的是明确说明哪些内容沿用了既有研究，哪些是新成果。”
此次发布展现了人工智能有望大幅提升数学研究速度的潜力，同时也提出了有关人类数学家角色的根本性问题。即使人工智能能够迅速生成复杂证明，验证和理解这些证明，并将其发展为新的研究成果，这一过程依然至关重要。
Eom Sangil 表示：“数学一直是在数学家相互合作、挑战问题，并在问题得到解决后深入理解、获得新见解的过程中发展起来的。如果大型语言模型让最难的问题变得轻而易举，我担心今后这一过程能否继续顺利进行。”
Baek Hyeongryeol 院长强调：“证明是否正确固然重要，但证明转化为我们知识的过程同样重要。无论人工智能产出多少证明，如果这些证明无法成为数学共同体中鲜活的知识，就很难说这本身就是数学的进步。”
版权所有 © 阿视亚经济。未经许可不得转载，禁止用于AI训练及使用。
