1500万美元！OpenAI联手Anthropic，请数学家给AI「验卷」
新智元报道
让三篇手稿一起翻车的，居然只是一处正负号错误：一篇出了错，另外两篇沿用了同一套构造，也被一并撤回。
10月15日， Simons基金会宣布，与OpenAI、Anthropic共同承诺1500万美元的资金及资源，支持数学家检验、理解并拓展AI成果。
OpenAI出资500万美元，另外提供模型和算力，希望将AI的进展转化为更深入的人类理解和新发现。
Anthropic承诺的500万美元支持，包含资金、算力和Claude使用权限。它也坦言：在数学乃至更广泛的科学研究中用好AI，需要时间、精力和资源。
说白了，就是支持数学家给AI验卷，把那些长篇证明读懂、讲清，再把有价值的方法用起来。
先公布10项涉及长期开放问题的研究成果，再宣布给出千禧年大奖难题——纳维–斯托克斯问题的证明，随后又集中发布数百篇数学手稿。
陶哲轩一针见血地指出，数学正从「证明稀缺」走向「证明充裕」，但人类的验证与理解能力未必跟得上。
MIT工程教育副院长Justin Solomon在播客节目里坦言，OpenAI那篇纳维–斯托克斯证明，自己读过开头几页，就读不下去了。
Solomon在《Odd Lots》播客中坦言，面对OpenAI给出的纳维–斯托克斯证明，自己连开头几页都没能读下去。
10月6日，OpenAI在GitHub公开这批来自内部未发布模型的成果，次日就在更新日志里留下了撤回3篇、修订14篇的尴尬记录。
按照论文约定本该取-1，AI在证明中却按+1计算。纠正后原以为归零的计数并不为零，所用定理的前提直接崩塌。
另外两篇手稿用了同一套方法，也被一并撤回，其中一篇研究的是K3曲面乘积的有理霍奇猜想。
约42%的主要结果配有Lean形式化材料，可供计算机检查推理过程。部分尚未形式化的结果，仍可能存在问题。
光知道算对了还不够，还要明白是怎样算对的：关键方法是什么？适用条件能否放宽？能不能用它解决其他问题？
大家争论的，已不只是三篇手稿有没有错，而是AI一口气交出这么多成果，谁来花时间查错、读懂，再把研究接着做下去？
10月7日，人类数学协会AHM发表严厉声明，批评这种一次性倾倒七百多个文件的行为是在「展示权力」，甚至呼吁数学家停止与OpenAI合作。
OpenAI应该 先发布经过Lean验证的手稿，其他材料单独放出来，请大家帮忙检查，别把验证过的和还没验证的混在一起。
MIT高级研究科学家Andrew Sutherland肯定了OpenAI迅速纠错的态度，但也表示，想要重新赢得信任，还需要更多工作。
大家担心的是：AI公司用学界拿不到的内部模型，抢先做出成果；数学家却因为缺少同样的工具，反而跟不上自己领域的进展。
普林斯顿高等研究院的顾问组（AGMAI）早在9月底就提出：AI实验室不能只顾着发布成果，也要出钱、出资源，支持人类把这些成果读懂。
但这些支持不等于买断话语权：学术界接受支持，也不代表学术界认可AI实验室的所有做法。
按照公告，基金会会公开征集项目，支持研究者检查AI成果、学习新工具，一起讨论这些工具该怎么用、按什么标准用。
AGMAI此前也建议，可以围绕复杂证明办暑期学校，或组织长期合作的研究小组，让大家有时间和资源把AI写的长篇证明一步步拆开、讲明白。
David Spergel在公告里强调，数学不应只被看作证明和定理的集合，更是由人类好奇心推动的集体理解。
不能只惊叹AI写出了多少篇论文，更要追问： 哪些结果经得起检查？别人能否理解并继续使用？这些成果带来了什么新的探索方向？
Simons公告明确提到，OpenAI和Anthropic提供的工具和算力，还会用到数学之外的基础科学研究中。
GPT-6 Astra被判错，专家复核后却发现，部分参考答案本身有错。修正后，Astra在TheoPhysEval的50道研究级题目中答对49道，正确率达到98%。