证明审计：找隐藏假设与逻辑缺口

写出证明草稿后，要像审稿人一样主动攻击。常见缺口包括除以可能为零的量、默认对象存在、只证必要性、遗漏边界、把图形直觉当一般事实，或在无限过程中偷用有限性。

逐行写依据

每一步标定义、题设、已证引理或标准定理。若只能写“显然”，尝试补一句；真正简单可以保留，补不出往往就是缺口。

检查定理前提

使用中值定理需连续与可导，交换极限积分需相应条件，有限维结论不能无说明推广无限维。引用时写出为何当前对象满足前提。

双向命题分开

“当且仅当”必须证明两个方向。存在唯一性需分存在和唯一；分类结果需证明所有列出的对象满足且没有遗漏。

边界与退化

空集、零维、参数为0、等号成立和最小规模常使一般步骤失效。把它们单列处理，不用“类似可得”掩盖。

同伴复核

让同伴只凭文字重建证明，不允许作者口头补充。其卡住位置就是文稿信息缺口。修订后用版本差异保存变化。

还可以反向检查每个条件是否真正被使用；从未出现的条件可能多余，也可能说明证明漏掉了关键环节。对自动证明或AI建议同样逐行审计。

任务：给自己的证明做前提清单、量词清单和边界清单，再邀请同伴找至少一个可改进点。