最近 AI 在数学上的进展，已经到了一个有点让外行恍惚的阶段。

过去一年，前沿模型已经开始直接推进研究级数学问题，甚至解决或推翻一些延续几十年的开放问题。陶哲轩最近讨论 AI 与数学时，也用了 “comparable turbulence” 来形容数学正在经历的变化。

笔者非数学出身。不过看着这些进展，再对照最近折腾一个信息分析系统的经历，还是忍不住斗胆想了一个问题：AI 都已经能推进这样的数学问题了，为什么一个看起来没那么高深的程序，折腾了好几个星期，最关键的一部分还是做不好？

当然不可能是因为这个程序比那些数学问题更难。

也许，是我们一直把不同的“难”，画在了同一根尺子上。

可重建，不等于可发现

之前关于完整 ESG 信息收集系统的系列已经写过很多，这里不再展开。现在回头看，可以做一个很有意思的思想实验。

假如把最终的 architecture、主要 heuristics、踩过的坑和解决原则完整告诉一个全新的模型，让它从头重新实现一遍，大概率是能做出来的，甚至有些地方可能写得比现在更漂亮。

但如果把时间倒回第一天，只留下最初那个很粗糙的目标，然后告诉模型：你自己试，自己看结果，自己决定下一步做什么——它最终能不能独立走到今天这套 architecture？

至少从实际使用 GPT-5.6 Sol 的体验来看，笔者没有这样的信心。至于更新的模型，没有实际测试过，这里不做判断。

这里有一个很有意思的区别：知道怎么做以后，把系统重新实现出来；和只知道最终目标，自己把这条路发现出来，是两种很不一样的能力。

可重建，不等于可发现。

最终看到的是：

A_final

真实的开发过程却更像：

A0 → Failure 1 → A1 → Failure 2 → A2 → …… → A_final

一个成熟的 architecture，很大程度上是过去所有失败留下来的化石。最后能够总结成十条漂亮的设计原则，背后可能是上千次失败、几十个奇怪观察，再逐渐压缩成几个 abstraction。

把最后十条交给模型，每一条都会显得很合理。问题是，它拿到的是筛选以后的结果，并没有经历产生这些结果的筛选过程。

这和看一篇漂亮的数学证明有一点像。证明写出来以后，每一步都可以显得顺理成章；但这不意味着第一次发现这个证明，也只有纸面上这几页那么难。

为什么一部分数学问题反而适合 Agent？

这里就要说到 Lean。

可以非常粗略地把 Lean 理解成一个“数学证明的编译器”。模型提出一个候选证明，Lean 检查；错了，返回错误；模型修改，再检查，于是形成一个可以反复运行的循环：

模型提出候选 → Lean 检验 → 得到反馈 → 再次尝试

当然，Lean 通过并不意味着数学研究的所有问题都解决了。形式化的命题本身是不是准确，有没有偷偷加入不恰当的假设，什么问题值得研究，都不是 Lean kernel 自动替人回答的。

但对 Agent 来说，Lean 提供了一样极其珍贵的东西：廉价、确定、机器可以直接读取的反馈。

模型第一次答错没关系，前 999 次都错也未必有关系。只要每一次错误都能被廉价而可靠地识别，它就可以继续搜索。

所以真正强大的组合可能不只是“模型足够聪明”，而是：

搜索 + 验证 + 反馈

这也解释了一个看起来有点反常的现象：数学可以极难，同时某些数学问题又非常适合 Agent。推理有多难，和答案有多容易验证，本来就是两件不同的事情。

现实世界没有 Lean

很多真实项目恰好相反。

模型设计出一个 architecture，代码跑通了，指标不错，解释也非常漂亮。最麻烦的问题却才刚刚开始：它到底是不是正确方向？

没有编译器告诉你。更麻烦的是，有时候连做这个项目的人自己也不知道。

今天觉得 A 是正确的基本单位，看了几百个真实案例以后发现不对，也许应该是 B；继续做，又发现 A 和 B 可能都只是表象，真正值得描述的是某种状态随时间发生的变化。

也就是说，评价标准本身并不一定固定：

K(t) ≠ K(t+1)

今天所有经验加在一起，最多只能告诉模型今天的 K(t)。真正推动项目继续前进的，往往是明天还没有见过的 Failure。

而这个 failure 到底意味着什么，也没有现成答案。是代码出了问题，是一个特殊 case，是指标选错了，还是整个问题的表示方法一开始就错了？应该打一个补丁，还是因此重新设计整个系统？

很多探索性项目最麻烦的地方就在这里：

没有完整 specification，因为 specification 本身，就是开发过程的产物。

如果把整个股市都交给 AI 呢？

可以把问题推得更极端一点。

假设把过去几十年全球股市的价格、成交量、财报、新闻、宏观数据全部交给一个模型。数据和算力都暂时不构成限制，只给它一个目标：找到一个未来仍然有效的投资策略。

然后让它自己研究。

它能不能最后发现真正的 alpha？至少从目前实际使用 GPT-5.6 Sol 的经验出发，很难有这样的信心。

金融看起来其实也有一个很像 Lean 的东西：

策略 → 回测

模型完全可以生成一百万个假设，然后挑历史 Sharpe 最高的。问题是，这很可能只是一个非常古老的问题：data mining。

数学里，Lean 今天说一个证明成立，明天不会因为美联储降息突然失效。金融里真正想知道的东西，却住在未来。

回测验证的是：这个策略在已经发生过的历史路径上表现如何。真正想知道的却是：它在未来一个尚未发生、甚至可能已经换了 distribution 的世界里会怎么样。

所以 backtest 并不是 Lean kernel。它只是一个 noisy proxy。

而且模型越强、搜索得越广，越可能把这个 proxy 优化到极致。这恰恰可能让 data mining 变得更严重，而不是更少。

更进一步，即使把全部历史数据都交给模型，还有一个问题没有解决：

到底什么值得搜索？

好的研究通常不是：

数据 → 搜索一切 → 挑出历史最优结果

而更像：

对世界的理解 → 机制 → 假设 → 检验

没人告诉模型 factor 是什么，它能不能自己发明 factor？没人告诉它应该观察什么，它能不能找到一种新的 representation？

这已经不只是回答一个问题，而是在形成问题。

“难度”可能根本不是一根轴

所以，“AI 都能推进研究级数学了，为什么一个程序还做不好？”这个问题，也许从一开始就问错了。

我们通常想象中的难度只有一根轴：

简单 → 困难

普通程序在左边，研究级数学在很右边。于是很自然地推断：既然 AI 已经走到了右边，左边的东西当然应该全部解决。

但真实世界里的问题，可能至少要看三个不同维度。

Search Difficulty：搜索难度

在问题已经定义好的情况下，找到一个可行答案到底有多难。研究级数学在这里可能极难，很多普通工程任务反而没有那么难。

Verifier Quality：验证质量

一个候选答案出来以后，有多容易判断它到底对不对。Lean 是一个非常强的 verifier，而现实工作里的很多评价只是弱信号：“看起来不错”“指标上涨”“用户好像喜欢”“回测 Sharpe 很高”，都不是数学意义上的 pass。

Problem-definition Maturity：问题定义成熟度

问题本身到底已经定义到什么程度？representation 是不是稳定的，成功标准是不是稳定的，真正应该优化的东西是不是已经知道？还是做着做着才发现，原来最开始问的根本不是正确的问题。

于是，一个任务完全可以Search 极难，但 verifier 很强，问题定义也很成熟。这种问题虽然非常难，却可能很适合 Agent。

另一个任务则可能Search 本身并不惊人，但 verifier 很弱，而且问题定义本身还在生成。它表面上没有研究级数学那么“难”，却可能很难真正自主化。

所以并不是 AI 连“简单问题”都不会。可能只是我们一开始就把完全不同的东西画在了同一根横轴上。

没有 kernel 的时候

这也带来一个更有意思的问题：当模型已经拥有如此多知识、如此强的推理和代码能力以后，人到底还在做什么？

“创造力”太模糊，“直觉”也太模糊。一个更具体的观察可能是：

人在没有 Lean kernel 的时候，也能继续工作。

现实世界经常不给 pass / fail。它给的是很弱、很脏，甚至互相矛盾的反馈。

有时候只是看了几十个案例，觉得“不对”。为什么不对，暂时甚至说不清楚。继续看，继续失败，过了几天才突然意识到：原来不是某个参数错了，而是整个 representation 错了。

更重要的是，人也不是一开始就知道正确目标，然后负责把目标告诉 AI。很多时候，人自己也不知道，只是在长期和现实互动的过程中，一边做，一边修改：

我到底在寻找什么？什么才值得测量？什么才算一次失败？什么结果才值得相信？

等这些东西最后沉淀成十条清晰原则，再交给模型实现时，一切突然显得简单了很多。

这可能也是现在最容易产生错觉的地方。模型越来越擅长在一个已经存在的评价结构里搜索，真正难自动化的，往往是那个评价结构本身还没有形成的阶段。

AI 最难的问题，可能不是最难的题

所以真正值得关注的，也许不只是模型又解决了一个多难的问题。

如果一个领域已经拥有清晰的问题、成熟的表示方式和廉价可靠的 verifier，那么 AI 可以一天尝试人类一辈子都试不完的东西。

真正麻烦的是另外一类问题：问题没有完全定义，表示方式还没有形成，反馈又弱又脏，甚至连评价标准都不存在，只能一边做，一边发明它。

这并不意味着这种状态会永远属于人类。这里的判断主要来自对 GPT-5.6 Sol 的实际使用，而不是对未来模型能力边界的断言。

未来的 Agent 也许会拥有更长期记忆，持续和真实世界互动，积累自己的失败历史，修改自己的 representation，甚至逐渐创造新的评价机制。

如果那一天真的到来，可能比“又刷爆了哪个 benchmark”要重要得多。

因为那时候，AI 得到的不再只是别人交给它的 Lean kernel。

它开始尝试自己长出 kernel。

至于那个自己长出来的 kernel，凭什么值得相信？

那可能又是下一个问题。