今天在一条很长的形式化证明链上栽了个跟头，又被一个独立的强模型一句话点醒，于是想把这件事背后的道理写下来——它关于一种我们天天在用、却很容易用错的东西：中间结论。

一、为什么要造中间结论

一个难定理，没法一口气从公理推到结论。人的办法是分解：把"我要证 $P$“换成"我先证 $A$，再证 $A \Rightarrow B$，再证 $B \Rightarrow P$"。这一串 $A,B$ 就是中间结论，是脚手架的关节。

这套办法在工程上好处巨大：

• 能分割。一条长证明拆成几块，每块边界清楚。
• 能给方向。隔离出"还差哪一步”，剩下的力气都往那一处使。
• 能并行。不同的块交给不同的人、不同的引擎同时啃，最后拼起来。

我这阵子做球面臂引理（Cauchy/Schoenberg–Zaremba 那条），就是一路这么往下剥：把一个球面的难命题，剥成一个折开臂的转角界，再剥成一个纯实数的"离散 Fenchel"命题，再剥成一个非退化的残差。每一层都更干净、更抽象、更像"只剩一个具体的小事实没证"。

二、可是有一种剥法，剥出来的是假的

分解的常见手法是抽象：我手上有个具体的真命题——“这条特定的、严格弯曲的臂，总转角小于 $2\pi$"——我不去用它的具体形状，而是抽出几条"相关的"性质（弱凸、相邻处严格左转……），陈述一个对所有满足这些性质的链都成立的一般定理，再把我的臂当成特例。

问题就出在这里：抽出来的性质，可能比原物的真实结构弱。

我那条臂是"严格弯曲、困在半球里、不可能拐成闭合多边形"的弧。可我抽象出的描述只剩"每处左转、各点都在每条边的左侧”——这套话也把一个长方形描述进去了。长方形四个直角，四次 $90^\circ$ 左转，总转角恰好

它满足我写下的每一条弱性质，却正好等于 $2\pi$，不小于。我那句"小于 $2\pi$"，在长方形上是假的。

换句话说：我把"具体真命题"翻译成"抽象命题"时，漏掉了让它为真的那一点结构——弧一直在弯、中间没有让它能拐成长方形的直边。漏掉的恰好是命题成立的根。

更阴险的是，随机数值验证完全没报警。我采样了几十万条凸臂，总转角全都小于 $2\pi$。可长方形是"完美直角"的退化构型，测度为零，随机采样几乎永远碰不到。“测了二十万次都没事"看着像铁证，其实系统性地避开了唯一的反例。

三、无根之木

“空中楼阁"这个词，本就出自《百喻经》。有个富人，见邻家三层楼气派，眼热的是最高那层，便也雇了木匠来造。木匠老老实实打地基、垒第一层，富人急了：「我不要下面两层，只把最上那间给我造出来。」木匠说，没有第一层哪来第二层，没有第二层哪来第三层。富人不依，只管要顶上那间——传为千古笑谈。

我今天做的，就是那个富人。我抱着一个抽象的"第三层”——一句漂亮的一般命题——以为踩着它就能够到结论，却没发现它底下的地基是假的，整座楼凭空悬在那里。

一旦那个抽象命题 $A$ 是假的，从它往下推出的一切——$A\Rightarrow B\Rightarrow C\Rightarrow\cdots$——逻辑可以步步合法，却全是空中楼阁。

因为 $A$ 假，就意味着永远没人能给出 $A$ 的证明。于是 $A\Rightarrow B$ 这块脚手架，看着结实，接口永远悬空：你要用它得出 $B$，得先递给它一个 $A$，而这个 $A$ 你递不出来。

这堆从假根长出来的东西，是无根之木，是沙上之塔，是水中月、镜中花。《金刚经》收尾那一偈说得透：「一切有为法，如梦幻泡影，如露亦如电，应作如是观。」它们自洽、漂亮、甚至能继续推出更多漂亮的东西，看着像那么回事，却抓不住、立不住，落不到实处——永远接不回你真正想要的那个结论。

四、可是——别怕——它污染不了你的真结论

这才是我今天真正想说的，也是形式化系统最该让人安心的地方。

我的合作者听到"假证明"时的第一反应是：那我的真结论会不会悄悄建在这堆沙子上？那岂不是我以为证好了的东西，其实靠着一个假引理？

不会。在 Lean 这样的形式系统里，假命题根本证不出来。

那些"假证明"长这样：

这是个完全合法的定理——蕴含式本身没错。但要用它无条件地得到 $P$，你必须先递进去一个 $A$ 的证明。而 $A$ 是假的，在一个一致的系统里，没有不作弊的办法造出这个证明。于是这条蕴含式就那么挂着，关节永远合不拢，$P$ 从来没被真正证出来过。

唯一能让脏东西接上真结论的途径，是有人用 sorry 或者一条假 axiom 把 $A$“硬凑"出来。而这正是 #print axioms 守着的门：它会把 sorryAx、把那条 axiom 原原本本列出来。只要你的最终定理是干净的（公理表里只有 propext、Classical.choice、Quot.sound 这三条标准的），它在数学上就不可能依赖任何假引理。

所以结论是：我的真结论现在的状态是**“还没证”，而不是“用假证明证了”**。这两者天差地别——前者是诚实的未完成，后者才是灾难。而形式化保证了我们只会落在前者。

对照一下纸面数学：一个"显然成立、细节略过"的假引理，可以无声无息地渗进整篇文章，几十页之后你引用它，自己都不知道脚下是空的。形式化不给这个机会。

五、更深一层：墙，是一种恩赐

最后这点最反直觉。

在纸上，假引理是沉默的毒——它不报警，悄悄往下传。在 Lean 里，假引理是响亮的墙——你想证它，怎么也证不出来，整条路就卡死在那儿。

我今天的错误，正是被这堵墙顶出水面的：一个常驻的证明 session 死活证不出那个残差，不是它不努力，是那东西本来就假。“证不出来"这个现象本身，就是系统在喊：你这里有根烂梁。再加上一个独立的强模型冷启动去证那个抽象命题，一搜就搜到了长方形反例——双保险。

墙不是阻碍，墙是诊断。 形式化把"沉默的毒"换成了"响亮的墙”，把"几十页后才暴雷"换成了"当场卡住”。这正是它值得托付的理由。

六、那么纪律是什么

中间结论的价值是真的：能分割、能并行、能给方向。但今天这一跤教会我一条配套的纪律——

大胆抽象去分解，但要狠心验真再往上building。

具体地：

1. “前提可满足"不等于"命题为真”。 一个残差可以非空（有实例满足它的前提），却依然假（结论在某个满足前提的实例上失败）。我之前把这两件事混为一谈，是病根。
2. 往上建之前，先试着证伪。 代数地、数值地找反例，重点扫退化与边界构型——平边、共线、首尾闭合、长度悬殊。随机采样会漏掉测度为零的反例，而临界情形恰恰住在那里。
3. 让一个独立的引擎来挑刺。 产出抽象的那个脑子，心里默认着它想要的那些实例，看不见自己把哪块结构丢了。冷启动的对手没有这个包袱，一上来就在整个抽象空间里搜反例。

抽象是为了看得更远，验真是为了站得住脚。两个都要。

后记：被点醒之后，那条链其实没废——最硬的那块解析归纳是对的，假的只是外面那层过度泛化的包装。把包装换成真实物体确实具备的、更强的几何事实，根就重新落地了。改日把这段几何接回去的过程，也许值得再写一篇。