第二十六章 一份证明需要哪些判断
一、先固定问题，再讨论谁能证明
当一份AI生成的文本标题写着“证明如下”，我们很容易直接进入推导检查。但在检查第一行之前，还有一个更早的问题：这份文本准备证明的，是否就是研究者原来提出的命题？如果目标已经变化，再严密的局部推导也不能自动完成原任务。
本章把证明判断分成相互衔接的几类对象：命题的含义、前提的范围、推理的有效性、依赖的状态、形式实现的对应，以及成果的研究作用。这些区分不是把一个证明拆成互不相干的部门，而是明确一个环节的完成不能代替另一个环节。
例如，程序成功接受一份形式化表达，能够为相应形式对象提供特定支持；研究者还需确认表达没有把原来的一般结论缩成特例，没有增加未经授权的条件，也没有通过记号变化改变问题。Lean官方验证指南也明确区分证明有效性与命题实际含义。[R3]
因此，AI数学证明的判断难题，不应只表述为“谁逐行看完这些文字”。更合适的组织单位，是一项项具体证明义务。每项义务要说明需要何种依据、由谁承接，以及完成以后可以对上层提供什么，而不是把所有状态压成一个绿色标记。
二、对象范围不是标题下面的装饰
命题中的变量属于什么集合，决定了结论究竟覆盖哪些对象。一个等式对非零实数成立，不等于对全部实数成立；某个有限集合上的结果，也不自动覆盖无限集合。对象范围不是为了显得严谨而添加的形式，它本身构成证明任务。
考虑断言“对所有实数x，x除以x等于一”。在通常实数除法的意义下，x等于零时表达不具有同样的定义条件。因此，正确的限定需要把非零要求写出来。若一套形式系统对零除法采用了总函数约定，还要特别确认该约定如何影响表达，不能把日常符号印象直接搬进去。
这里可以看出语义判断的两种工作。一种检查变量和运算在什么范围内有意义；另一种检查当前形式约定与所研究的数学问题是否一致。它们都可以由专业工具帮助，却不能因为字符相同就视为已经完成。
对于复杂对象，范围还可能隐藏在类型、结构实例或引入的默认条件中。研究者不必每次展开所有定义，但应在目标建立与边界变化时明确检查。封装的恰当作用是保存这些条件，而不是使它们从任务记录中消失。
三、一个量词次序，能够改变整个任务
比较两个关于自然数的命题。第一个说：对每个自然数x，都存在一个自然数y，使y大于x。第二个说：存在一个自然数y，使它大于每个自然数x。两个命题使用相同的变量和比较关系，但量词次序不同，意义也完全不同。
第一个命题成立。给定任意x，取y=x+1，就有y大于x。这里选择的y可以依赖x。第二个命题不成立：假定存在这样的y，只需在“每个x”中取x=y，就会要求y大于自身，产生矛盾。一个局部见证不能变成对所有对象统一有效的见证。
这个例子不需要复杂计算，却显示了高层任务中的细粒度判断。一处量词顺序的改变，影响的是整个研究结论。因而，层级高不等于只看大意；某些决定任务身份的细节，必须在目标层被保留。
AI若把第一种结论写成第二种，检查者不能只说“这段需要润色”。需要回到命题结构，明确依赖关系。若程序把依赖x的构造存成一个无条件常量，也需要检查形式化接口，而不是只修订自然语言。
量词还揭示为什么“我为很多对象都找到了一个例子”不能证明存在统一对象。每次成功可能使用不同见证。记录成功次数而不记录依赖方式，会把一种任务的证据误用于另一种任务。后面逐点收敛与一致收敛的区分，正会把这一问题推进到函数序列。
四、前提的增加、删除与等价改写
设原任务是由A推出C。证明过程中，AI发现只要再有B就容易完成，于是给出A与B共同推出C的证明。这个证明可能完全有效，但它完成的是另一个条件命题。只有进一步从A证明B，或者明确取得修改任务的授权，才能说明它与原目标的关系。
删除前提也需要依据。若已经证明A与B推出C，不能因为B在最终表述中显得冗长，就把它删去。需要检查证明是否真正使用B，或另给一个不需要B的证明。条件摘要不是修辞压缩，而是逻辑接口。
有时前提只是等价改写。例如，在通常实数次序中，x大于零与x非负且x不等于零等价。要把这种改写用于自动系统，可以保存等价依据，而不是把任何语气相近的描述都当成同一条件。任务身份可以通过已证明的等价关系保持，不必机械要求每个字符完全不变。
因此，目标登记应同时容纳两种情况：语义等价的表示变化，以及实质不同的命题修订。前者可以在保留依据后作为同一任务的不同表示，后者则需要新版本或新目标。严谨不等于禁止改写，而是使改写的性质清楚可查。
五、证明错误与命题为假不是一回事
发现推导中有缺口，只能先说明当前论证没有完成相应任务，不能立即推出命题为假。一个真命题可以有很多错误证明，一个假命题也可以有局部看起来正确的计算。判断需要保留“此证明未成立”与“命题已被反例否定”的区别。
例如，某人声称前 n 个正整数之和公式可以由观察前三个值直接推出。这个论证不充分，却不意味着被猜测的公式必定错误。后续可以寻找数学归纳法、代数恒等式或其他一般论证。错误判断若过早关闭目标，就可能阻断本来值得继续的研究。
反过来，一个确实满足原条件而违反结论的反例，能够否定全称命题。这里的证据义务包括反例属于对象范围、满足全部前提，以及结论在该对象上失败。少掉任何一项，都可能是一个看似反例而实际越界的对象。
这一区分对状态设计很重要。可以记录候选证明有缺口、目标仍开放；也可以记录原命题已否定、需要研究替代目标。不能把所有未通过都写成“错误”，再让下一轮无法知道究竟是证明策略需要改变，还是目标本身需要修订。
六、局部推理如何接受检查
在一个固定的数学语境中，推理步骤需要由相应规则和已经取得的条件支撑。若已知P以及P蕴含Q，可以推出Q；若只知道Q以及P蕴含Q，则不能一般地倒推出P。方向很小，结果可能很大。
用整数性质说明这一点：一个整数能被四整除，则它为偶数；某个数为偶数，却不一定能被四整除，二就是例子。把充分条件当必要条件，是可以通过局部关系检查发现的错误。若解释只是重复“显然”，检查并未完成。
计算步骤也可能需要边界条件。由ax=ay消去a，通常需要a非零；由两边平方得到的结果，反推原等式时还需处理符号信息。一个运算可以保持某一方向的蕴含，却不保持双向等价。证明记录应当知道当前在使用哪一个方向。
细粒度检查不必总由人逐项口头完成。符号工具可以承担某些计算，证明助手可以检查形式规则，研究者可以在较粗层级检查策略与语义。关键不是谁看起来最忙，而是相应义务有没有被有能力的机制承接。
七、计算发现、数值检验与一般证明
数值计算可以帮助发现模式、寻找反例和定位错误，却需要与一般证明区分。若命题涉及无限多个对象，有限个成功案例通常不能直接覆盖全部对象。它们可以支持继续研究某个猜想，而不能仅凭数量把猜想升级为已证定理。
也不能由此把计算一概排除在证明之外。对于明确有限的对象集合，如果确实穷尽了全部情况，计算过程又得到适当验证，就可能构成证明的一部分。某些无限问题也可以通过严密论证归约到有限检查。关键在覆盖依据与检查可靠性，而不是人是否手工完成计算。
因此，应当分别保存数值观察的范围、误差或表示条件，以及从这些观察到目标结论的推理桥梁。如果桥梁尚未建立，状态就是证据或启发，而非完成。浮点近似尤其不能在没有误差说明时自动替代精确等式。
在本书的机制中，计算模块可以形成封装，但其接口要说明输出是什么：精确值、带保证的区间、近似结果，还是启发性猜测。不同输出类型能承担不同义务，不能在进入自然语言报告时统一改写成“证明表明”。
八、形式检查的支持范围与信任边界
形式工具的重要价值，在于把一部分推理检查组织成可以反复调用的机制。使用者不必重新手写每一步规则，却能够获得比单纯阅读流畅文本更明确的依据。然而，形式系统也在特定逻辑、实现和任务表述中工作，不是一个不需要任何条件的终极裁判。
Lean的公理说明区分了证明与直接加入的公理。系统可以追踪一个定理使用了哪些公理及依赖；如果随意引入不相容的公理，就可能破坏整体推理基础。sorry所形成的未完成依据也能够通过相应依赖检查被发现。[R13]
本书从中提取的设计原则是：完成状态必须关联当前采用的基础与依赖。研究者可以在某套明确公理下研究条件性结果，但不能把它写成不依赖这些条件的结论。形式化不是免除前提说明，而是有机会使前提关系更清楚。
信任边界还包含程序运行环境、输入对象及检查器本身。是否需要更强复核，应随任务风险和输入来源调整。本书不报告本项目已经运行了Lean验证，也不把以下自然语言推导称为经过形式内核检查；二者的证据状态应当分开。
九、证明构造与证明接受不必由同一机制承担
一个系统可以使用高度探索性的方式寻找证明，包括尝试许多失败路线；接受结果时，则要求另一套较稳定的检查机制。构造阶段允许产生候选，接受阶段不能仅凭候选产生者的确信度改变标准。这种分工适合封装，也能保留探索空间。
例如，AI提出一个新引理，系统先把它登记为候选；经过证明及相应核验，才允许它作为已证依赖。若暂时找不到证明，可以把它用于条件性探索，但上层结果必须明确依赖尚未解决的条件。开放问题可以进入研究，不能冒充已经闭合的基础。
这种状态区分还保护研究者免受“每次都必须成功”的压力。能够明确说出在哪一步停止、缺什么条件、哪些局部仍然有效，本身是一种可使用的研究结果。它让下一轮能够从真实位置继续，而不是从漂亮但虚假的完成状态开始。
封装成熟因此不要求生成过程从不犯错。更合理的要求是：错误和缺口不能未经相应处理就穿过接受边界，被上层当作已完成成果使用。高铁类比中的安全承接，在数学这里表现为对证明义务和状态的实际承接。
十、证明的研究作用，需要另一层判断
一个命题被证明，不等于它自动具有重大研究价值。它可能是已有结果的直接重复，也可能与原来的问题关系很弱；反过来，一个尚未证明的猜想也可能提示重要方向。证明有效性与研究作用相关，但不是同一维度。
研究作用可以包括提供新连接、澄清必要条件、缩小问题范围、产生可再使用的方法，或者揭示某条路线为何不可能。具体价值需要结合研究任务说明，不能把“新”这个字当成独立保证。新错误并不因为新颖而成为定理。
在本书的框架里，三方程使我们追查成果与支撑过程的关系，六路径使我们判断研究如何进入和推进，三原理则参与对重组及整体形成的评估。它们作用于整个研究活动，而不是在形式证明通过后另贴三枚装饰性标签。
例如，一个更短证明可能暴露结构，帮助推广；也可能隐藏关键条件，使教学和后续调用更困难。长度本身不能决定价值。需要说明为什么这次压缩保留了必要差异，又使什么新的关系进入可理解范围。
十一、一张证明义务记录应怎样组织
本书建议以目标为中心，而不是以输出文件为中心保存记录。目标需要有稳定身份、版本、自然语言说明和相应形式表达；前提与允许使用的基础单独列出。这样，文稿改名或格式变化不会自动改变任务状态。
对每个依赖，记录其结论、适用条件、证明状态和来源位置。对每项检查，记录检查对象、采用方式、实际结果以及未覆盖的范围。自然语言审阅、程序测试和形式证明应分别标注，不能因为都叫“检查”就合并成同一种证据。
状态变化应保留原因。候选变为已证，需要相应依据；已证模块的定义或依赖版本改变，可能需要重新确认；发现反例，应使相关上层目标返回合适状态。记录不需要保存每次无意义的生成细节，但必须保留影响结论身份的变化。
这张记录不是让研究者增加一份永远没人看的表格。它应服务于当前判断：明确哪些可以整体使用，哪些需要展开，哪些问题值得转交。若字段不能参与任何后续决定，就应考虑精简，而不是把记录数量当作严谨程度。
十二、为什么形式化翻译本身也要进入发生诊断
从自然语言到形式语言，不只是把词语换成符号。定义的选择、对象的表示、隐含条件的显式化，都可能改变问题结构。一个形式化过程可以帮助发现原来语言中的歧义，也可能把歧义过早固定为某一种便利解释。
例如，“存在一种方法对每个输入都有效”，究竟要求同一种方法，还是允许随输入更换方法？如果原文没有说清，形式化时的量词安排便承担了实质判断。不能在程序通过后倒过来说原文从一开始就具有这个唯一含义。
发生诊断要保存这种选择：原来有哪些可能解释，为什么采用当前版本，哪些使用者或领域依据参与了决定。如果后来发现与研究意图不一致，就应修订目标映射，而不是责怪检查器没有理解自然语言。不同环节的职责需要清楚。
这种诊断也不意味着形式化永远无法可信。经过明确协商、标准定义和交叉检查，许多表达可以形成稳定的语义封装。重点是让它的形成可说明、边界可检查，而不是把翻译既神秘化又当作一次完成的透明步骤。
十三、一个局部证明失效以后，怎样不丢掉全部工作
设一个证明有三个相对独立的引理，其中第二个存在缺口。若系统把整篇文稿一概删除，就可能丢失第一和第三个已经有效的结果；若一概保留完成标记，又会让缺口继续传递。合适的处理需要依赖结构。
可以先标出直接依赖第二引理的节点，重新审查这些节点的完成状态；不受影响的模块仍保留原有依据。若后续找到第二引理的替代证明，再按实际连接重新验证。这样，修复具有范围，而不是在全盘否定与全盘相信之间摇摆。
当然，某个看似局部的问题也可能影响共同基础。例如定义改变、对象范围改变或共享假设被否定，影响可能跨越多个引理。依赖记录应能揭示这种共享联系，不能仅按文稿段落位置估计影响大小。
这一机制体现发生学诊断的实际价值：错误不是抽象污点，而是有形成位置、传播路径和修复范围的差异。定位越清楚，越可能保留真实成果并减少重复劳动。判断与创造因此不是对立关系，恰当的判断组织能够为继续创造保存条件。
十四、由一份证明，进入证明能力的发生
本章没有把数学判断交给某一个固定主体，也没有要求研究者永远亲自重做全部推导。它把一份证明所包含的不同义务显露出来，使人、AI和验证工具能够围绕明确对象形成协作。构成解释从这里落实为工作组织。
关键边界是：任务身份不能在流畅表达中改变，前提不能在封装中丢失，依赖不能由名称自动获得已证身份，检查器的支持范围不能被扩大成全部研究价值。这些边界不是阻止工具成熟，而是使成熟具有可依据的内容。
当这些义务能够被稳定承接，研究者才可能把已完成模块作为整体使用，进一步比较结构、修改目标并提出新问题。下一章将研究这种模块怎样构成：什么可以被折叠，哪些信息必须留在接口，以及模块之间怎样形成能够重新展开的证明网络。
一份数学证明至少把目标含义、推导有效性和研究用途带到不同的判断位置。它们相互支持，却不能由一个“通过”标记统一代答。保留这些区别以后，研究者才可能安心折叠某些局部过程，集中考察较大的结构。证明模块如何保存前提、结论与依赖，便成为封装从口号进入数学工作的关键；接下来将逐项展开这一接口。