AI能写出人类看不懂的数学证明吗？

当AI的证明超出人类理解

Lex Fridman的播客中出现了一个颇为反直觉的设想：如果AI给出一个数学证明，而这个证明并非因为太长，而是因为其中的想法让该领域所有专家都摸不着头脑，人类该怎么办？

对话者的回答带着逻辑学的冷峻：推理规则只有寥寥几条，公理也只有寥寥几条。在这种约束下，产生"不可理解的数学"的唯一途径几乎就是规模。换句话说，理解的门槛可以被推高，但数学的底层语法依然是有限的。

这个判断本身值得玩味。它把"不可理解"从神秘主义拉回到工程问题——不是数学变成了魔法，而是搜索空间大到了人类认知难以在有限时间内完成重构。

形式化与直觉的张力

对话中抛出了一个"逆向"问题：去形式化（unformalizing）数学会是什么样子？形式化让人类对结果的正确性有了信心，但人类理解一个结果的方式，很大程度上停留在非形式化层面——什么才算有趣的特例？这个技巧从哪里来？它和哪些问题平行？

这引出两种常被混为一谈的东西：证明的工程（engineering of the proof）与证明的传播（communication of that to someone else）。对话者指出，这两者在写论文时几乎是对立的。工程追求严密，传播追求可感的叙事。

实分析课上的"倒叙"实验

对话者分享了自己教实分析的经历。任何实分析教材的开头都是构造实数——用有理数柯西序列的等价类来定义实数，花掉大约两周，然后回到数轴，再开始ε-δ微积分。他的疑问是：上课之前学生就已经知道实数是什么，就是那条数轴；两周之后数轴又回来了，中间那两周到底为了什么？

他的做法是倒过来教：直接进入ε-δ计算，做上六周，直到撞上波尔查诺-魏尔斯特拉斯定理——有界实数序列必有收敛子列。这个定理在有理数上不成立，在实数上成立。为什么？实数到底是什么？直到此刻，学生才会真正追问构造问题。

这正是"讲述"与"建构"的分野。若目标是搭建理论，必须先构造对象；若目标是讲故事，完全可以从直觉出发，直到直觉撞墙为止。

波尔查诺-魏尔斯特拉斯定理（Bolzano–Weierstrass theorem）是实分析中的基本定理之一：实数集 ℝ 中任何有界无限序列都含有收敛子列（其极限也在 ℝ 中）。它之所以在教学中被当作关键节点，是因为它揭示了实数系与有理数系的本质差异——同样的命题在 ℚ 上不成立，例如 √2 的有理近似序列有界却不在 ℚ 中收敛。这条定理的成立依赖于实数的完备性（least upper bound property），而完备性又正是柯西序列构造实数所要保证的核心性质。因此，当学生在这条定理上"撞墙"时，倒叙教学便自然地把他们引回"实数究竟是什么"的构造问题，这正是对话者设计教学路径的用意。

数学不是定理的涨潮

对话者明确反对一种数学观：数学只是定理数量的持续上涨，因此AI贡献定理怎么可能有害？他的反驳是，数学远不止定理的计数，还包括与问题搏斗的过程。

一个好问题会反击。在搏斗中，研究者发现更一般的意义，建立起一套信念与抽象的体系。这套体系才是数学的实质部分，而定理只是它在某个坐标下的切片。

由此推演出一个对AI时代的写作判断：未来的论文形态会大不相同——更多篇幅用于讲述"我在这条路上学到了什么"：标准步骤在这里、那里，卡点出现在哪里，为什么选择向左而不是别的方向；同时附上一份精简的形式化，确保工程上站得住。

故事不能单独存在。数学不是音乐，不能靠优美的平行声部就绕过规则——巴赫可以那样做，数学不行。

数学中的"问题反击"可以对照数学史上的经典案例来理解。希尔伯特在1900年提出的23个问题、韦伊猜想、朗兰兹纲领，都曾以"反击"的方式重塑整个领域：为解决一个问题而发明的工具（如理想、层、上同调）往往比原问题的解答更重要。这与对话者所说的"与问题搏斗产生更一般的抽象"是一致的。换言之，数学的实质增长常常表现为概念体系的扩张与重组，而定理数量只是这种扩张在形式化层面的投影。理解这一点，就能明白为何"AI多产定理"本身并不自动等同于"数学的进步"。

黑箱证明与理解的二次外包

回到最初的问题。如果AI给出一个人类读不懂的证明，一种务实的路径是：让另一个LLM来讲解这个故事，把证明拆成更易追问的小问题，逐步重建对"它究竟怎么得到答案"的理解。

这里有一个隐含的层级：证明可以被逐行验证，却仍然不被理解。验证与理解不是同一件事。对话者反复强调，人类想要的是故事，是理解，而不只是正确性证书。

这也解释了为什么"规模"这个答案既成立又不令人满足。规模能解释为何证明超出人类的重构能力，却解释不了为何人类仍然执着于把它讲成故事。而后者，恰恰是数学作为人类事业的部分。

形式化验证与理解的区别在数学基础中有清晰的对应。形式化证明是一串符合推理规则的符号序列，可以由计算机逐行核验（如 Lean、Coq 等证明助手所做的那样）；但"理解"涉及的是语义层面的把握——为什么这个证明会成立、关键引理从何而来、哪个步骤承载了实质想法。逻辑学中早有区分：一个证明可以是有效的（valid，形式上正确），却不一定是可理解的（intelligible）。哥德尔不完备定理之后的证明论研究也表明，形式可验证性与人类可重构性之间没有必然的等价关系。这正是对话者所说"验证与理解不是同一件事"的技术背景。

对AI数学的一点冷思考

把这段对话放回当下的AI数学讨论，有几个判断值得记住。

其一，形式化验证的价值会随AI产出增加而上升，但形式化不是终点，它只是让工程可信的最低保障。

其二，AI在数学上的真正贡献可能不在于定理数量，而在于能否提供可被人类吸收的中间叙事——哪些特例值得看、哪条路径为何被放弃。这类"过程性知识"目前仍是稀缺品。

其三，"与问题搏斗"这一隐喻指向一种难以外包的认知活动。问题反击的时刻，正是新抽象诞生的时刻。若AI跳过搏斗直接给出答案，人类得到的可能是正确却无法生长的知识。

对话没有给出终局答案，但它把问题从"AI能否做数学"推进到"人类想要的数学究竟是什么"。这个转向本身，比任何单一结论都更有价值。