AREX Feed Article
开发者 Daniel San 复核 openai/math：未见「sorry」或伪公理，但命题与原问题的对应仍待核验
10 月 7 日上午（北京时间），开发者 Daniel San（）在 X 上发布了他对 OpenAI 数学仓库 openai/math 的复核。他称自己克隆并检视了这个仓库，在 Lean（一种把证明逐步写出来、由计算机逐步检查的编程语言）代码中搜索了「sorry」与伪公理这两类常见「捷径」，都没有发现；但他指出，Lean 只验证证明步骤，不验证形式化命题是否就是原问题，而 OpenAI 自己在仓库文件里把这批形式化的审查状态标为「未经检查」。
这次复核针对的是 OpenAI 于美东时间 10 月 6 日傍晚公开的 。仓库的说明文件 README 称，收录的 722 篇数学手稿及配套证明工件由内部模型产出，归入 372 个家族（每个家族归组若干相关论文）；OpenAI 在中称，一直在与 Institute for Advanced Study（IAS）数学与人工智能独立顾问组磋商，发布方式参考了其建议与公开推荐。
一次从「sorry」查起的复核
按他的复述，这批材料的来历是：OpenAI 有一个新的内部模型，常规数学基准对它已经不够难，于是把职业数学家尚未解决的开放问题交给它，其中一些已悬置数十年；评估一共提出约 4,000 道题，模型在每道题上花约 3 小时，把答案写成正式论文；经过筛选，留下收录进仓库的手稿。他说，其中一些结果声称解决了广为人知的问题。
他的检查重点是两类「捷径」。「sorry」是 Lean 里用来跳过未完成证明步骤的写法；伪公理则是把未证的命题直接声明为公理。这两类写法都能让形式化文件表面通过，实际并没有真正完成证明。他称自己在 Lean 代码里搜索了这两类写法，都没有找到；他还说，超过一半的结果带有 Lean 版本。他把这部分称为仓库里证据最强的结果，其余部分则基本上是「AI 说它成立」，仍需要人工审阅。
机器检查不到的一环
按 Daniel San 的解释，Lean 会逐步检查写出来的证明：只要编译通过，推理的每一步就都成立，就像一个「从不疲倦、从不跳过任何一行的老师」。但有一个环节它不检查：用 Lean 写下的那个命题，是不是论文声称解决的那个著名问题。
「问题稍微写错一点，你就能完美地证明一件错的事。」他写道。他还称，已经有人发现，某些 Lean 形式化只覆盖了论文主张的一部分。
形式化目录与 README 里写明的限制
仓库文件里能找到相关记录：Lean 形式化目录（）中，review 部分的 status 字段写的是 unchecked，即「未经检查」。Daniel San 在帖文里说的「OpenAI 自己就把这些形式化标为未经检查」，在仓库里可以看到对应的标注。
仓库 也给出类似的说明：收录的结果处于不同的验证阶段，并非都有配套的 Lean 形式化；未形式化的结果中「有些可能存在问题」，OpenAI 称会尽力尽快修复这类问题。
剩下的核对与数学家要的「收据」
Daniel San 在帖文中说明，这只是初步复核，还有更多内容要查；这条复核并非同行评审。Scientific American 在中写道，这批成果将需要数学家花几个月来消化和理解，包括判断这些证明里究竟有没有新想法，还是主要是现有技术的拼接。
外部核对的范围，也取决于 OpenAI 公开了哪些内容。据该刊报道，OpenAI 没有公开模型，也没有公开 prompt（提示词），只披露了单个问题的平均算力等少量统计；OpenAI 还称，正尽快且负责任地推动模型发布。MIT（麻省理工学院）数学家 Andrew Sutherland 对该刊说，在模型公开、结果能被复现之前，关于「单个 agent（智能体）一次性解题」的说法都应视为未经核实，「我们应该要求看收据」。
仓库 README 称，OpenAI 会继续补充新的 Lean 形式化，并正在探索由社区托管的仓库来承载这批材料；而按 Daniel San 的说法，命题与原问题的对应，仍需要有人来核对。