一个循环，让 GPT-5.5 和 Claude 攻破了 9 个未解难题

有个搞理论计算机的教授，被一道题折磨了两年。

不是那种查查文献、跟学生讨论一下午就能松口气的题，是躺在床上闭着眼还在脑子里转、转到天亮的那种。这道题后来发在了 FOCS 2023，作者栏里有他的名字，Omri Weinstein。理论 CS 圈里，FOCS 是顶会里的顶会，能在那儿留个未解的口子，说明这题是真硬。

前几天，他自己的这道题，被人用两个大模型接起来的一个小循环，给解了。

他没绷住，跑到 X 上发了一条。大意是，连 OpenAI 前阵子那个 Erdős 突破都没能说服我「大模型能做通用数学研究」这件事，但这回，我改主意了。用一个很巧的「证明者-验证者」循环，这套东西一口气搞定了 9 个实打实的理论 CS 未解问题，其中一个，让我失眠了整整两年。

一个原本的怀疑者，被 AI 解掉了自己心头那根刺。我看到这条的时候，第一反应不是「AI 好牛」，是「嘶……这个反转有点意思」。

先把事情本身说清楚。

干这事的是彭炳辉（Binghui Peng）带的一个小组，还有 Runzhou Tao、Steven Wang、Hantao Yu 几位。彭之前在哥伦比亚，现在是 Google Research 纽约的访问研究员，2026 年 1 月要去马里兰大学计算机系当老师，正经做机器学习理论和理论 CS 的人。不是那种蹭热点发 demo 的团队，这点先记着，后面有用。

他们做的东西，说穿了朴素得有点让人意外。没有训练新模型，没有什么秘密武器，就是搭了一条很短的管线。GPT-5.5 Pro 当证明者（prover），负责生成证明；Claude Opus 4.8 当验证者（verifier），负责挑错、把关。两个模型在一个循环里来回过招，一个写，一个挑刺，写了改改了写。最后论文用 Claude Code 组装起来，作者本人再润色、核对一遍。

就这么个结构，解了 9 个公开的未解问题。

我得先把这 9 个是什么摊给你看，不然「未解难题」四个字太容易被想象成民科口中的「哥德巴赫猜想」了。它们分三堆。

一堆是 COLT 的公开问题榜，占 4 个。COLT 是学习理论的顶会，每年会挂一批「谁能解出来算谁的」的公开问题。这次解掉的包括 shuffled SGD 的那组不等式（Yun、Sra、Jadbabaie 在 COLT 2021 提的）、线性回归里的无权重数据选择（Hanneke 等人 COLT 2025）、稳健条件概率估计（Langford，COLT 2010，这题挂了十几年了）。还有一个学习量子电路的（Kun 和 Reyzin，COLT 2015），标注是 partial，只解了一部分，这个细节我特意留着，等下说。

一堆是交换代数（commutative algebra）里的，来自 Glaz 等人整理的一份公开问题集，也是 4 个，编号 4、20、27、30(c)，涉及 finite-conductor 环、整值多项式这些东西。跟上面的学习理论完全是两个世界的数学。

最后那 1 个，就是开头 Weinstein 失眠两年的那道，在线杠杆分数采样（online leverage-score sampling）的对抗鲁棒性，FOCS 2023，作者里有 Jiang、Peng、Weinstein。你没看错，Peng 就是这次干活的彭炳辉本人。所以这事更微妙了，他们不光解了别人的题，还顺手把自己组几年前留下的坑给填了。

（另外还挂了个 Erdős 问题 477，tiling complement，跟总数的算法有点重叠，就不单算了。）

好，事实铺完了。现在聊我真正觉得值得唠的三件事，因为热闹是热闹，但热闹底下藏着的东西才是我关心的。

第一件，也是我最想让你记住的，关键根本不在某个「超级模型」，而在那个循环。

你注意到没有，这里面没有任何一个模型是被神化的。GPT-5.5 Pro 不是靠自己一个人硬刚出 9 道题，Claude Opus 4.8 也不是。真正干活的是「prover 出证明，verifier 挑错，来回迭代」这个结构。单拎出任何一个模型，直接问它这道 FOCS 2023 的题，大概率给你一堆看着挺唬人、细看全是窟窿的推导。数学证明这东西最要命的地方就在于，错一步，后面全废，而且模型特别擅长「一本正经地错」。

那怎么办？让另一个模型专门盯着挑刺。

这套思路，做工程的朋友应该秒懂，它就是我们天天在干的事。让模型真正能干活的那层工程，给它搭脚手架的那层，核心从来不是「换个更强的模型」，而是「怎么把模型的输出兜住」。你光让 AI 生成，它就飘；你得在它旁边架一个验证的环节，跑测试、对类型、挑逻辑漏洞，不通过就打回去重来。prover-verifier 说到底就是把这套「生成-校验」的循环，从写代码搬到了证明数学定理上。

我一直觉得，这两年真正被低估的进步，不在模型参数，在这些「怎么把模型接起来用」的编排上。大家盯着榜单看谁家又涨了两个点，但生产环境里让 AI 从「能说」变成「能交付」的，往往是那个不起眼的验证循环、那个失败重试、那个超时看门狗。这次这条数学管线，等于是把这个道理，用一种特别硬核的方式又演了一遍。厉害了，简单的东西接对了，能出这么大的活。

第二件，就是开头那个反转，怀疑者被自己的题打了脸。

我特别喜欢 Weinstein 这条 endorsement，因为它太不「营销」了。你想，如果是彭他们自己吹「我们解了 9 道题」，你我大概率一笑而过，谁还不会写个 README 呢。但背书的人是被解问题的原作者，而且这人前面还公开说过「OpenAI 的 Erdős 突破都没说服我」。一个立场如此鲜明的怀疑者，在自己蹲了两年的题被解开之后改了口，这种被说服，比一百条 benchmark 都有说服力。

说真的，我们这行最不缺的就是 hype。什么「AI 重塑科研」「大模型赋能数学」，这类话我听得耳朵起茧，一看到就想划走。但一个真研究者盯着自己的题、确认它真的被解开、然后不情不愿地承认「我错了」，这种时刻是装不出来的。数据点是死的，人是活的。从一条推文里，我能想象出他半夜盯着屏幕反复看那份证明、一边验一边嘀咕「不会吧不会吧」的样子。那个画面比 9 这个数字动人多了。

第三件，也是我觉得最不该被热搜标题吃掉的，这事的边界，其实挺诚实的。

你回去看那个 partial。学量子电路那道题，人家自己标了「部分解决」，没往脸上贴金说全解了。再看 GitHub README 里那句话，证明是模型生成的，但论文是作者「polished and verified」，润色并验证过的。翻译成人话就是，模型出草稿，人做最后一道关。不是你按个回车，AI 自己把 9 篇论文端到你面前，全对，签收就行。中间有大量人类数学家在盯、在核、在判断哪条能用哪条是幻觉。

我为什么要专门拎出来讲这个？因为这恰恰是这件事最可信的地方，也是最容易在传播里被磨掉的地方。标题党会写成「AI 独立攻克 9 大世纪难题」，但真相是「一条 AI 管线加一群会验证的人，解了 9 个真实但不算世纪级的公开问题，其中一个还只解了一半」。后面这句一点都不性感，可它是真的。而真诚这东西，是唯一的捷径，工具有边界就说边界，AI 会幻觉就承认会幻觉，这样你说它牛的时候，别人才信。

3Blue1Brown 的 Grant Sanderson 前阵子在 Dwarkesh 的播客里聊 AI 和数学，有句话我记到现在。他说 AI 在 IMO 拿金牌，不等于 AGI，那只是又一个被攻克的基准而已；哪怕将来它把千禧年大奖难题解了，人类还有一大堆活儿是没法被自动化的。我觉得这个冷静的调子，正好配这次的 9 道题。它是真突破，值得高兴，棒棒的；但它不是终点，也不是神迹，它是「生成-验证」这套朴素工程，在数学这块最硬的地里，又往前拱了一寸。

写到这我想起「小岛AI」这个名字里的航海意思。这波 AI 做数学，特别像航海，你以为大模型是那艘越造越大的船，其实真正让你不撞礁的，是船上那套一遍遍校验航向的罗盘和流程。船再大，没人核对坐标，照样开进暗礁里。这条 prover-verifier 管线，干的就是罗盘的活。

所以别只盯着「9 道题」这个战果。想想那个循环，想想那个改了口的怀疑者，想想那句诚实的 partial。真正的信号藏在这三样里，而不是热搜的字号里。

想自己看原始材料的，我把链接放这儿。彭炳辉团队的项目在 GitHub（github.com/Pengbinghui/pipeline-math），他放出成果的原帖在 https://x.com/binghuip/status/2070756087998152855 ，Omri Weinstein 那条改口的背书在 https://x.com/WeinsteinOmri/status/2071940117875282030 ，彭本人的主页在 https://www.cs.columbia.edu/~binghuip/ ，Grant Sanderson 那期对谈在 https://www.dwarkesh.com/p/grant-sanderson-2 。都是一手的，别信我转述，自己去看。

说真的，我看完这一圈，最大的感触不是「AI 要取代数学家了」，恰恰相反。是那个循环里，模型负责猛冲、猛试、猛错，人负责在最后一道关口说「这个对，那个不对」。冲的部分交给机器，判断的部分留给人。这分工，我看着挺舒服的。