10道数学难题,24小时反转新智元
10项数学难题,24小时反转。
这个周末,OpenAI与Anthropic两大AI巨头,在数学的最前沿短兵相接。
先是8月1日,OpenAI研究员Sébastien Bubeck宣布,他们未公开的下一代主力模型Astra,一口气证明了10项前沿数学成果,还甩出了10份Lean证书、10份逐题思路复盘。
别小看这10个问题。
它们的主要结论至少10年没人推动过,不少一搁就是几十年,是货真价实的开放难题。
虽算不上数学里最深的未解之谜,却个个都是难啃的硬骨头。
Epoch AI旗下FrontierMath的负责人Elliot Glazer直言:光是非索菲克群这一篇,就肯定能进数学界公认的顶级期刊Annals of Mathematics。
这10道难题一甩出,AI圈直接炸了,有人当场喊出「数学奇点已经到来」。
Anthropic这边迅速接招。
不到24小时,研究员Levent Alpöge在Bubeck的帖子下回了一句:「我用Fable完成了一半。」
紧接着他又补充,自己做出来的是OpenAI榜单上的第4、5、6、7、8项,一共5项。
实验条件,Levent称很干净:完全自主、通用提示词、全程无网络,为了防止OpenAI的解法泄漏进上下文,还特意加了一层防护。
当然,Levent目前还没放出Fable的完整证明细节,他表示会上传。
但如果得到证实,这件事的分量就变了:
OpenAI用未发布的模型Astra抢到的首发先机,只保住了24小时。而追上来的Fable,是Anthropic早就公开、人人都能调用的模型。
一项「数学首发」保鲜期只剩24小时
网友Chubby转帖:「公开可用的Fable,复现了Astra一半成果。」
评论区有人调侃:这么看,OpenAI是不是只抢到了一个首发?
过去,一项数学成果的优先权之争,通常以年为单位。
谁先想到、谁先证出、谁先发表,中间隔着漫长的投稿、审稿、修改。
而现在,Astra还没正式发布,它公布的成果,仅仅24小时,就已经被一个公开模型追平了一半。
首发的含金量还在,但保质期却大大缩短。
不少网友已经在喊「数学奇点」,两个AI巨头也紧紧咬上了。
2000美元背后还有更贵的账
OpenAI还甩出一个数字:找到这10项解法,成本不到2000美元。
按研究员Noam Brown的说法,它对应的是寻找这些解法所需的token,再按Sol API价格折算出来的。
也就是说,这只是成功跑出10个解法那一刻的边际推理成本。
在这之外,还有Astra本身的训练研发、那些试了却没成功的问题、人类把论证整理成249页论文的工时、把每个证明形式化成Lean的成本,以及最后外部数学家审查的成本。
Noam自己也承认,他们还尝试过其他重大问题,但都没成功,千禧年大奖难题一个都没拿下。
即便如此,2000美元仍然把AI解出一道前沿难题的边际成本,打到了地板。
有人甚至调侃,OpenAI是不是明天会再公布10项数学突破,或者等到下周一次发100项。
从「互相刷榜」到「互相验货」
Fable去重做Astra的同一批题,这件事要比普通刷榜有意思得多。
刷榜测的是已知答案:题目和标准答案都摆在那儿,比谁分高。
而两个模型在无网络、防泄漏的条件下,各自独立抵达同一个前沿结论,测的是完全不同的东西:这个结果到底可不可靠,能不能被独立复现。
这更像同行评审。
Levent目前只是在X上「作出了声明」,并没有放出那5项证明的PDF、提示词、完整运行日志、token成本或Lean证书。
网友Haider质疑:就算是真的,为什么要用Fable去复现Astra,而不是直接拿它去解新的开放问题?
事实上,Fable并不是只会蹭Astra热度,它也会解新题。


