几何证明验证不是检查最后一行是否写出了目标结论，而是检查从已知条件到结论之间是否存在一条连续、合法、没有循环的推理链。一个答案即使结论正确，只要使用了尚未满足前提的定理、把图形直觉当作已知，或者暗中调用了目标结论本身，就不能视为完整证明。
一套可复用的检查方法，应当同时覆盖四个层面：命题是否被准确理解、每条定理的使用条件是否满足、相邻步骤能否真正推出下一步，以及整条证明是否避开自我引用与下游定理。数形智拍(GeoSnap)的“原理”把这些关系放进定理知识图谱，使“这一步依据什么”能够被追溯到明确节点。
什么是几何证明验证？ 几何证明验证是把一份证明拆成“已知—推导—依据—结论”四类信息，逐步检查每个推导是否由已知条件、公理或已经成立的定理支持，并确认最终结论确实到达命题目标，且没有偷换条件、关键跳步或循环引用。
关键结论
- 正确结论不等于正确证明，验证对象是整条推理链。
- 每次引用定理时，都要同时验证该定理的使用前提。
- 图上“看起来相等、平行或共线”不能自动成为证明依据。
- 合法的省略应当可以补全；无法补全的关键跳步是逻辑缺口。
- 使用目标定理本身或其下游结论证明目标，会形成循环论证。
- 自然语言 AI 可以辅助检查证明，但结果具有概率性；形式化证明器提供更强保证，却要求先把命题精确形式化。
为什么只核对答案不能验证几何证明？
证明的价值在于建立“为什么成立”，而不是重复“它成立”。 两份证明可以得到同一个正确结论，其中一份每一步都有合法依据，另一份可能恰好猜中结果，却在中间使用了错误关系。
可以把证明看成一条带标签的路径：
已知条件
↓ 依据 A
中间结论 1
↓ 依据 B，并满足 B 的全部前提
中间结论 2
↓ 依据 C
目标结论
验证时不能只看节点，还要检查箭头。每一条箭头都必须回答两个问题：前一步是否提供了足够信息？标注的定理是否真的适用于当前图形？
这也是几何自动推理比普通数值计算更困难的原因之一。2024 年的 AlphaGeometry 研究指出，将几何题转换为机器可验证表示本身就很困难；系统需要让语言模型提出辅助构造，再由符号推理引擎按照明确规则进行演绎。Nature 论文 这说明“找到一个可能的思路”和“确认每一步都成立”是两个不同任务。
一份几何证明应该检查哪些部分？
完整检查可以分为七项：目标、已知、对象、定理前提、推导连续性、依赖合法性和结论闭合。 这七项既适用于手写证明，也适用于 AI 生成的自然语言证明。
| 检查项 | 核心问题 | 常见问题 |
|---|---|---|
| 1. 命题目标 | 最终要证明的究竟是什么？ | 把充分条件写成必要条件，或只证明了部分结论 |
| 2. 已知条件 | 哪些信息是题目明确给出的？ | 把图上比例、共线或垂直关系当作已知 |
| 3. 对象定义 | 点、线、角和辅助对象是否定义清楚？ | 突然出现未定义点或方向不明的角 |
| 4. 定理前提 | 每次调用的定理是否满足全部条件？ | 只看到相似外形就调用相似判定 |
| 5. 推导连续性 | 当前步骤能否推出下一步？ | 省略了决定性的等量、全等或比例关系 |
| 6. 依赖合法性 | 引用的结论是否已经成立？ | 用目标定理或其后续推论反过来证明目标 |
| 7. 结论闭合 | 已证明内容是否与目标完全一致？ | 推到相近结论后停止，没有完成最后一步 |
检查顺序很重要。若命题目标或已知条件识别错误，后面逐行检查再严密也没有意义；若定理前提不满足，仅凭最终式子正确也不能修复这条链。
第一步：把命题改写成“已知—求证”
验证开始前，先把自然语言题目压缩成明确的已知集合和目标集合。 这一步是在固定推理边界：证明只能从已知、公理和允许调用的既有定理出发。
例如，两条不同直线 $\ell_1$、$\ell_2$ 交于点 $O$，点 $A,B$ 在 $\ell_1$ 上且分居 $O$ 两侧，点 $C,D$ 在 $\ell_2$ 上且分居 $O$ 两侧。目标是证明：
$$ \angle AOC = \angle BOD. $$
这里可以使用的已知包括：$OA$ 与 $OB$ 是相反射线，$OC$ 与 $OD$ 是相反射线，两条直线不同。图上两个角“看起来一样大”不属于已知。
命题改写还要避免方向偷换。例如，“若两直线平行，则内错角相等”与“若内错角相等，则两直线平行”是两个方向不同的命题。即使两者都可能成立，也需要分别引用对应定理。
第二步：为每个推导补上依据
每个实质性步骤都应能标注为定义、公理、已证定理或基本代数变换。 如果一句话无法归入任何一类，就需要检查它是否只是直觉描述。
继续验证“对顶角相等”。由邻补角关系可得：
$$ \angle AOC + \angle AOD = 180^\circ. \tag{1} $$
同样，由另一组邻补角可得：
$$ \angle AOD + \angle BOD = 180^\circ. \tag{2} $$
由 $(1)-(2)$ 消去共同的 $\angle AOD$：
$$ \angle AOC = \angle BOD. $$
这份证明的依赖非常短：几何部分只调用“邻补角之和为 $180^\circ$”，随后使用等式相减。数形智拍的图谱因此把“邻补角”连接为“对顶角相等”的直接前置，而不是把两条定理仅仅归在同一章节。
第三步：检查定理的全部使用条件
引用定理名称只是开始，真正的验证对象是“当前图形是否满足该定理的全部前提”。 定理可以完全正确，但使用场景不满足条件，推导仍然无效。
以相似三角形为例，常见错误是看到两个三角形外形相近，便直接写“所以相似”。合法推导需要给出 AA、SAS 或 SSS 等相似判定所要求的角或边比例；若使用 SAS 相似，还要确认相等的角是两组对应边的夹角。
可以使用下面的三问法检查一次定理调用：
- 当前要调用的定理是什么？ 写出完整名称，而不是“由性质可知”。
- 它要求哪些前提？ 把定理前提逐项列出。
- 以上前提各自在证明的哪一步已经得到？ 若找不到来源，就存在缺口。
公理化体系的价值正在这里。Birkhoff 在 1932 年提出基于尺度与量角器的平面几何公设时，核心目的之一就是把距离和角度关系放在严格、公开的基础上。Birkhoff 原论文 前提越明确，后续定理调用就越容易核查。
第四步：区分可以补全的省略与关键跳步
自然语言证明允许省略显然且可机械补全的细节，但不能省略决定结论是否成立的桥梁。 判断一处省略是否合法，可以尝试把它展开为若干原子步骤。
例如，从 $x+y=180^\circ$ 和 $z+y=180^\circ$ 得到 $x=z$，中间的等式相减通常可以省略，因为它能够唯一、直接地补全。相反，从“两边分别相等”直接跳到“两个三角形相似”，就需要先确认相等的是哪些边、是否成比例，以及是否具备夹角关系。
可使用一个简单标准：
如果补全省略步骤只需要通用逻辑或基础代数，它通常是可接受的简写；如果补全需要猜测新的几何关系、添加辅助线或调用未说明的定理，它就是需要显式写出的关键步骤。
数形智拍的自然语言校验不会要求证明与标准答案逐字一致。不同辅助线、不同定理组合或不同书写顺序都可能形成合法证明；检查重点是这些步骤能否到达目标，而不是复刻唯一模板。
第五步：检查循环论证和非法依赖
循环论证是指证明在不同名称或中间形式下，实际使用了正在证明的结论。 在定理知识图谱中，这可以转化为一个结构问题：证明目标节点时，不能引用目标节点本身，也不能引用依赖目标节点才能成立的下游结论。
假设定理 B 的证明依赖定理 A，那么可以用 A 证明 B；反过来，在尚未建立 B 之前，不能再用 B 或 B 的推论证明 A。否则图谱中就会出现闭环：
A → B → C
↑ │
└───────┘ 非法：C 又被用来证明 A
自然语言中的循环不总是显眼。证明可能不直接写目标定理名称，而是引用一个等价命题、逆命题或下游公式。因而，验证需要把引用名称解析回图谱节点，再检查它是否落在目标节点的后继集合中。
数形智拍的证明校验采用“模型判断 + 确定性图谱规则”的组合：视觉语言模型负责读取手写页面、理解自然语言步骤和识别引用；代码层再根据真实依赖图检查自引用与下游引用。低置信度的明确判定还会进入更怀疑性的复核流程。模型负责理解表达，图谱规则负责守住可计算的逻辑边界。
AI 可以验证几何证明吗？
AI 可以辅助验证自然语言几何证明，但不能把概率性判断描述成绝对正确的形式证明。 它适合识别命题、读取图形与手写步骤、寻找缺失前提和解释问题；若要获得机器核验级保证，需要把命题和每一步推理转换为形式语言，并交由证明内核检查。
可以把当前方法分成三个层级：
| 验证方式 | 优势 | 局限 |
|---|---|---|
| 人工阅读 | 能理解省略、图形直觉和多种表达 | 标准可能不一致，难以大规模重复 |
| 视觉语言模型 + 图谱规则 | 能处理照片、自然语言和定理依赖 | 仍可能误读或误判，需要保留不确定结果 |
| 形式化证明器 | 每一步由小型可信内核检查 | 命题形式化成本高，普通书写不能直接输入 |
Lean 官方文档说明，Lean 的核心内核只负责检查 proof term；这类设计能够提供强验证保证，但前提是所有对象、命题和推理规则已经被精确编码。相比之下，照片中的自然语言证明更容易提交，也更接近日常书写，却必须接受概率模型的不确定性。
AlphaGeometry 采用神经模型与符号引擎组合，也体现了相同分工：神经模型建议有创造性的辅助点和辅助线，符号系统依据形式规则完成可靠但较慢的演绎。Google DeepMind 技术说明 后续的 AlphaGeometry 2 在形式化后的历史 IMO 几何题上扩大了覆盖范围，但 Google 同样明确说明，题目需要先完成形式化。AlphaGeometry 2 说明
数形智拍如何把证明检查变成可追溯流程？
数形智拍原理把证明校验连接到同一张定理知识图谱：命题、标准证明、合法前置和禁止引用的下游结论来自同一份结构化数据。 因此，反馈不只说“可能有问题”，还可以指向缺失的依赖或发生阻塞的步骤。
当前流程可以概括为：
- 读取证明页面：支持多页照片，保留页面顺序和图形信息。
- 确定目标命题：绑定当前定理的陈述、前置节点与参考证明。
- 提取推理链：识别关键步骤、定理引用、辅助构造和最终结论。
- 判断是否到达目标：检查证明是否真正推出完整命题。
- 执行依赖门控：代码检查自引用、下游引用和循环关系。
- 输出可操作反馈：分别列出成立的关键点与需要补全的位置。
这不是形式化证明器的替代品。它的目标是让自然语言证明拥有更清晰的检查框架，并把可确定的依赖规则从概率模型中剥离出来。
更多关于图谱节点和依赖边的构建方法，可阅读《从 4 条公理到 138 条定理》。数形智拍产品页面展示了图形重绘、逐步证明与原理图谱之间的关系；其他研究内容收录在 ByuTech 博客。
一份可以直接使用的证明检查清单
提交或保存一份证明前，可以逐项回答：
- 我是否准确写出了已知条件和完整目标？
- 每个点、线、角及辅助对象是否已经定义？
- 是否把“图上看起来如此”误当成已知？
- 每个关键等式、平行、垂直、全等或相似关系是否有来源？
- 每次调用定理时，它的全部前提是否已经满足？
- 省略步骤是否能够仅用基础逻辑或代数直接补全？
- 是否引用了目标定理、等价改写或依赖目标才能成立的结论？
- 最后一行是否与求证目标完全一致？
- 如果存在另一条合法证明，当前检查是否允许不同路径而非强制模板？
这份清单的核心只有一句：对每一步持续追问“依据是什么”，直到答案回到已经声明的公理、已知条件或已证结论。
常见问题
AI 判断“证明正确”是否等于形式化验证通过？
不等于。自然语言 AI 的判断来自概率模型，即使结合图谱规则也需要保留误判和无法判断的可能；形式化验证则要求把命题与证明编码为严格语言，由可信内核逐步检查。两者在输入便利性与保证强度之间存在明显取舍。
几何证明可以和标准答案使用不同方法吗？
可以。合法证明不要求与参考证明逐字相同，也不要求使用同一条辅助线。验证应检查当前路径是否满足前提、避免循环并确实到达目标，而不是检查文本相似度。
什么样的跳步可以接受？
能够通过基础逻辑或代数唯一补全、且不会引入新几何关系的省略通常可以接受。如果补全过程需要猜测辅助线、补充未说明条件或调用新的关键定理，就应当显式写出。
为什么证明知识图谱能发现循环论证？
因为图谱记录了每条定理的前置与后继。验证目标定理时，可以确定性地禁止引用目标本身及其下游节点，从结构上阻止“用结论或结论的推论证明结论”。
图形画得不准确会影响证明吗？
证明依据的是命题给出的关系，而不是图片比例。示意图可以帮助发现构造，但不能单独证明等长、等角、平行或共线；这些关系仍需由已知条件或合法推导建立。
结语：验证的是推理链，不是最后一行
一份可靠的几何证明，应当允许每个关键步骤被追问、展开和回溯。命题界定边界，定理提供规则，知识图谱记录依赖，校验流程则检查这些元素是否真正连接成一条没有断点和回路的路径。
可以从一个最短案例开始：打开数形智拍的原理与证明图谱，选择“对顶角相等”，尝试只使用“邻补角”重新写出证明，再用上面的清单逐项检查。
参考资料
- Euclid, Elements, Book I.
- George D. Birkhoff, A Set of Postulates for Plane Geometry, Based on Scale and Protractor, Annals of Mathematics, 1932.
- Trinh et al., Solving Olympiad Geometry without Human Demonstrations, Nature, 2024.
- Google DeepMind, AlphaGeometry: An Olympiad-level AI System for Geometry, 2024.
- Google DeepMind, AI Achieves Silver-medal Standard Solving International Mathematical Olympiad Problems, 2024.
- Lean, The Lean Language Reference.
- Pashler et al., Organizing Instruction and Study to Improve Student Learning, Institute of Education Sciences.
- 数形智拍产品与原理图谱, ByuTech.