OpenAI发布722篇数学论文，如今需收拾残局

OpenAI上周向代码托管平台GitHub一次性上传了722篇数学论文，这些论文针对的是数学领域4000个未解问题的大规模攻关成果。消息一出，数学界仍在消化这批材料，而且恐怕还要消化很长一段时间。表面上看，这是一件史无前例的事，但实际上历史上有一些先例可以帮助我们理解刚刚发生了什么，以及接下来应该怎么办。 先回答两个核心问题：这波数学论文洪流对AI意味着什么，对数学又意味着什么？关于第一个问题，我们现在有了进一步确认——领先的AI模型基本上可以一键生成看起来达到研究水平的数学成果。OpenAI使用了一个未公开的内部模型，并声称每项结果平均消耗了相当于“3小时ChatGPT Pro思考算力”的资源。Pro是OpenAI最高端的产品，月费在100到500美元之间。当然，“平均”这个词在这里弹性很大，而且OpenAI的订阅服务享受大量补贴，所以很难给出每项结果的真实成本，OpenAI也没有提供具体数字。不过，平均每个问题所需的投入似乎远不及该公司上个月公布的纳维-斯托克斯方程成果——OpenAI称那项工作耗时约88小时，据报道成本高达1500万美元。OpenAI做这件事，并不是因为它想要一台数学机器，而是因为数学是能够拉伸其模型能力的试验场之一。 数学能力出色，是否意味着OpenAI即将在其他科学领域达到类似水平，或者接近其宣称的通用人工智能（AGI，即能完成人类所有任务的AI模型）目标？我认为并非如此。数学有一个对AI成功至关重要的核心要素：可验证性。AI能否写出媲美莎士比亚的戏剧，没有客观标准来衡量；但数学有，因为一个证明要么为真，要么为假。通过将证明形式化——把逻辑步骤转化为名为Lean的计算机代码，让计算机进行机械校验——AI公司可以证明它们确实做到了所宣称的成果。这为提升AI的数学能力提供了一个便捷的闭环：让模型生成证明，将其形式化，然后根据准确性给予奖励。其他领域缺乏这样的闭环，这很可能使AI模型更难取得进展。 OpenAI此次发布特别值得关注的一点是，其形式化工作并不完整。量化这一点有些棘手：在其Lean证明目录中，722篇论文里只有162篇的主要结果完成了形式化；而附带任何Lean代码的最新结果列表显示，722篇论文共372个“家族”中，只有235个家族有代码伴随。无论怎么算，工作都没有完成。这就引出了对数学界的影响问题。至少对于已形式化的证明，数学家可以较为确信论文是准确的（仍存在Lean版本与文字版本不完全对应的可能，而且OpenAI的这些结果尚未经过核查）。对于其余论文，OpenAI把这项苦差事留给了数学家。加州大学洛杉矶分校的陶哲轩此前将这种情况比作“把生肉尸体倾倒在我们的公共村桌上”。那么，OpenAI为什么没有完成形式化工作？可能有几个原因。第一个是，它可能感受到了压力。