证明之后：机器、数学与理解的门槛

尤金·维格纳据说在看到计算机完成一项复杂的量子力学数值计算后，说过这样一句话：

“很高兴计算机已经理解这个问题了，很好。但现在，我也想理解它。”

我查了很久，没有找到确切出处。它更像一段口耳相传的轶事。维格纳1960年倒是有另一句有据可查的话：“数学语言在表述物理定律时的恰当性，是一种奇妙的恩赐，我们既不能理解也不配拥有。”但我仍决定保留前一句——无论它是不是维格纳说的，它都精确地切中了当前人工智能全部成就与全部局限之间那道最深的裂隙。

在我自己使用AI辅助数学研究的日常经验中，这种感受尤为强烈。计算机理解了一个问题，至少，它产生了一个正确的答案。但人没有。人仍然站在理解的门槛之外。

数学家威廉·瑟斯顿在1994年的《论证明与数学进展》中把同一个意思说得更彻底：数学的目标不只是生产定理和证明，而是推进人类对数学的理解。证明的价值不仅在于确认真伪，更在于人能够从中获得洞察。作为一名经常与形式化证明系统（如Lean）打交道的数学家，我对此深有共鸣。形式化验证可以告诉你逻辑链条没有断，但它无法告诉你这条链条为什么存在。

将这两句话并置，便是我对当前大语言模型全部进展的基本判断。

2026年8月4日1日，OpenAI发布报告：其下一代模型Astra对十个长期开放的数学与理论计算机科学问题给出了新结果——包括非sofic群的显式构造（推翻自1999年以来的核心猜想）、Connes刚性猜想的否证、Ehrhart体积猜想的证明，以及三个Erdős问题的解决。数学论证主要由模型产生，人类负责整理；随后模型将证明形式化为Lean 4证书，公开发布。据估算，搜索这些解法所消耗的token按API价格约为两千美元。

必须承认：若其中多数结果经独立审查后成立，这是大事。在我参与过的各类数学竞赛和评分中，我们往往是在考察人类寻找已知答案的能力。但开放问题则截然不同：在此之前，无人知道结论是否成立，也无人知道证明应该长什么样。能在群论、算子代数、复杂性理论、编码理论和极值组合等差异极大的领域中持续产生可供专家审查、可形式化验证的新论证，这已经表现出某种异于传统基准测试的研究能力。菲尔兹奖得主Tim Gowers此前对Astra五月发现的Erdős单位距离猜想反例表示“会毫不犹豫推荐在《数学年刊》发表”——尽管这并非对十项成果的全部背书。

但“AI已成为成熟的数学家”仍然太早。

Lean证书可以验证形式系统内的推导是否成立，我完全信任这一点。但作为数学家，我们深知形式化只是证明的终点，而非起点。它不能回答更根本的问题：使用的假设是否合理？形式化过程中是否悄悄改变了问题？证明引入了新思想，还是极其复杂地组合了已有技术？它改变了人们对一个领域的理解，还是仅仅关闭了一个问题？这些问题不能由proof checker回答，仍需数学共同体判断。

评价Astra，至少需要区分两套指标。成功率是工程指标；成果的正确性、重要性和解释力才是科学指标。从数学史看，一个系统尝试一百万次，最终产生一个改变领域的证明，这个证明不会因前九十九万九千九百九十九次失败而贬值。人类数学家同样花费数年乃至数十年走过大量未发表的歧途——我自己就有过为了一个猜想尝试数月却一无所获，最终在完全不同的语境下找到突破口的经历。数学最终不按“每小时证明多少定理”来评价。真正要看的是：有没有找到新的结构、新的概念、新的思维方式；方法能否迁移；其他数学家能否从中学到东西，并由此提出下一批问题。

如果Astra的多数成果最终得到确认，这件事最可能被历史记住的，不是“AI打败了数学家”，而是：从这一天起，产生证明不再必然是数学研究中最稀缺的能力。 选择什么值得证明，解释为什么成立，发现其中真正的新思想，并将其转化为人类可以使用的理解——这些反而变得更加重要。

这里需要做一个澄清。Astra展现的数学推理能力，与持续学习能力，是两个不同的问题。但它们在更深处相通，共同指向同一个困境：当前神经网络缺乏人类可寻址、可局部更新、可稳定冻结的结构化知识表征。

这并非说神经网络内部没有任何结构。机制可解释性研究已经揭示，模型确实会涌现出某种结构：高层语义概念往往以近似线性的方向编码在表征空间中；事实关联在Transformer的前馈网络层中有相对可定位的“知识神经元”；稀疏自编码器甚至能从纠缠的激活中解耦出数以千万计的、近单义的特征。结构是存在的，但它是涌现的、统计性的、全局耦合的。

人类的认知结构则不同。人脑的知识是可寻址的。神经网络的“超叠加”效应表明，它试图将比参数维度多得多的特征压缩进同一个低维空间。特征并非正交的独立基向量，而是以近乎正交但不完全正交的方向叠放。这意味着，知识确实“大致”在某处，但这个“某处”是统计可定位的，而非工程可寻址的。你能在激活层面事后找到它，却不能在不牵动大量纠缠邻居的前提下精确改写它。

这种全局耦合正是持续学习瓶颈的根源。麦克洛斯基和科恩1989年首先系统描述的灾难性遗忘，并非更多数据或更大模型能消除的缺陷，而是这种知识存储方式的必然结果。为写入新知识而调整的每一个权重，都在通过非正交方向的干扰悄悄改写旧知识。人学会煮咖啡，不会因此忘记骑自行车；数学家掌握了一个新领域的工具，不会因此忘记代数几何的基本定理。但在这里，稳定性-可塑性权衡成为一道难以逾越的鸿沟：太容易学新东西，就容易忘掉旧东西；太努力保住旧东西，就难以适应新环境。

人脑的解法极其精巧。麦克莱兰、麦克诺顿和奥赖利1995年的互补学习系统理论描述了这一架构：海马体高可塑性，一次接触即可保存具体事件；大脑皮层高稳定性，通过数月反复练习慢慢整合长期统计规律。快速学习与慢速巩固通过睡眠连接，双速并行。

而当前LLM占据了两个糟糕的角落。对话中“快而不存”——每次都能迅速响应，关掉窗口一切归零。重新训练则“快而乱存”——权重被全局更新，新覆盖旧。唯独“快而稳”这个档位——既能快速捕捉新信息，又能将真正重要的东西稳定整合进长期结构——至今无人知道如何制造。所谓技能、记忆等外挂方案，本质上是在不更新模型权重的前提下造了一个粗糙的外部海马体。我们让模型去检索RAG文档，就像给一个失忆症患者塞了一本笔记本。但稳定整合的问题基本没动。如果一次权重更新就能让模型对某个窄问题的认知一致性发生变化，它如何支撑后续数年的连贯研究？

而那些相信人类专家不可替代的人所说的护城河——几十年攒出来的判断力和品味——恰恰是AI因缺乏可稳定整合的结构而无法获得的东西。

明白了持续学习与可寻址结构的缺失，再看大语言模型另外两个常被讨论的“瓶颈”，会发现它们在根源上相互关联。

长上下文，本质上是把经验写不进可寻址结构这一事实的补偿：既然学不会，就把所有该知道的事写成小抄，每次对话前塞给模型看。小抄越做越长，但读小抄和学会是两回事——每次从头读，太长会看漏，下次见面一切重新开始。在我处理大型形式化项目时，这一点尤为明显：如果上下文太长，模型会忘记几万行前定义的变量。当然，长上下文并非仅仅是持续学习的替代品；处理一部长篇、一个大型代码库或一场复杂对话，需要在工作记忆中同时保持大量信息，这与长期记忆互补。但其边际成本——每次重新加载、注意力在长序列中衰减——正是持续学习缺席的直接代价。

稀疏奖励对人之所以不致命，是因为每一次教训都会长进脑子里，日积月累攒成直觉。在数学研究中，我们经常面对数月没有正向反馈的猜想，但每一次失败的尝试都在重塑我们对问题的直觉。奖励信号在时间上分散，但人脑能将其结构化地整合进长期知识。LLM做不到：稀疏反馈无法被累积和内化。

三者不在同一层次。持续学习是最根本的一个。若真正解决，长上下文和稀疏奖励的压力将大幅减轻。但在解决之前，后两者仍有独立的工程价值——它们是模型在无法学习的前提下，勉强扩大有效工作范围和提升判断精度的补偿手段。

由此，对AI替代就业可以给出一个更清晰的判据：你的工作是否依赖非普遍性的长上下文？是否依赖随时更新的环境？是否依赖非普遍性的判断？三项皆“是”，则在持续学习突破之前你是安全的；三项皆“否”，则你只是还没轮到。

现在将两件事并置。

其一：Astra可以产生新证明，Lean可以验证推导，但Lean不能告诉你这个证明是否引入了新思想、是否改变了对一个领域的理解。理解的验证，仍然需要人。

其二：LLM无法持续学习。知识一次性灌入，对话归零，重训则覆盖。快与稳不可兼得，因为它缺乏一个人类可寻址的结构化系统来分别处理快速学习与慢速巩固。

这两件事表面独立，深处相通。它们都指向同一个事实：当前AI系统既不能像人一样理解，也不能像人一样学习。

理解需要稳定性。你不能今天说圆是到定点距离等于定长的点的集合，明天改变主意。数学定义之所以可靠，正因它们不因新训练数据而漂移。但稳定性恰是当前神经网络最缺乏的。

学习需要可塑性。你必须将新经验融入已有结构，而非每次从头开始。但可塑性在神经网络中表现为全局权重更新——旧知识被覆盖，新知识无法局部写入。

稳定与可塑的不可兼得，是同一个问题的两个侧面。神经网络的知识没有可寻址的结构，既不能被局部更新，也不能被局部冻结。你不能指着几百万个权重说“这部分是圆，不要动”。一切知识弥散于一切权重，动一处则全局皆动。

这正是Phaenarete ASI Lab目前正在探索的方向。

我们不解决持续学习。我们探索另一个同样根本的问题：即使模型能力停滞在当前水平，即使它不能像人一样学习和理解，能否让它的输出变得可审计？

这个方向不声称替代理解。可审计性不能让模型“真正理解”数学——它只能让人类事后检查输出，核对每一个语义承诺是否与原始问题一致。它不能保证模型内部推理可靠，但可以保证模型外部输出可追溯。在当前技术条件下，这是工程妥协，不是根本解决方案。但它可能是目前唯一不需要等待神经科学突破就能推进的方向。

在我自己推动数学形式化的过程中，我深刻体会到“可审计”的价值。技能与记忆是对持续学习瓶颈的工程妥协。EFS——我们的受控中间语言——是对可寻址结构缺失的工程补救。两者面对的是同一个更深层事实：当前神经网络既不能像人一样学习，也不能像人一样被问责。

我们需要让模型在每次推理之前，先把“我理解了什么”写下来——以人类可读的形态学标记签字画押。不是让模型学会煮咖啡而不忘记骑自行车，而是让模型在煮咖啡之前先写下一句：“我认为咖啡是这样煮的。”然后人可以指着那行字说：“这里，你错了。”这与我们在Lean中拆解证明步骤的逻辑如出一辙：不追求一蹴而就的完美，只追求每一步的清晰可查。既然内部不可寻址，就让模型在外部用可寻址的语言签字画押。

必须诚实承认：如果模型自身都没有正确的“理解”，它写下的“理解”是否可信，本身就需要审计。这是可审计性方向的根本局限——它不能创造理解，只能暴露理解的缺席。

维格纳说：“很高兴计算机已经理解这个问题了。但现在，我也想理解它。”瑟斯顿说：“数学的产品是清晰和理解，不是定理本身。”

两句话之间，横亘着当前AI的全部成就与全部局限。它可以产生证明，验证证明，找到人类数学家一生找不到的结论。但它不能告诉你：这个证明为什么成立，背后的思想是什么，它与哪些领域有联系，它改变了我们对什么的理解。

它不能做这些，不是因为不够聪明，而是因为它的知识没有人类可寻址的结构——不能被局部访问，不能被独立验证，不能被稳定保存和更新。

我们无法在神经网络内部重建这种结构。但可以让它在外部写下结构——以一种人可以阅读、核查、指认的语言。这不是对理解的替代，而是对理解的辅助。当AI的推理可以被审计，人的理解才有可能跟上。

工具会变。科学家的具体职责会变——我自己就经历了从纸笔到Mathematica，再到Lean和LLM的多次工具迭代。但科学的目标不变。我们不是为了证明而证明，不是为了计算而计算。我们最终想要的，从来不是更多答案，而是更多理解。

而理解的第一步，是看见。看见机器在想什么，看见它在哪一步做出了什么承诺，看见它在哪一个词上犯了错。

在这个AI既能解开放数学题、又学不会煮咖啡的奇特时代，这座审计的桥可能是通往理解的唯一路径。它不宽，也不稳。但它是目前唯一不需要等待一个神经科学突破就能开始建造的东西。