一条几何定理不会因为被印在书上就自动成立。它要么是体系公开接受的起点，要么能够由定义、公理、题设、合法构造和已经证明的结论一步步推出。第一性原理学习几何，就是持续追问每个结论的来源，直到到达不再依赖更早定理的基础。
数形智拍(GeoSnap)把这种追溯变成可浏览的证明图谱：节点表示公理或定理，箭头表示证明实际调用的前置。它不要求每次都从公理重写全部细节，而是让封装后的定理随时能够被拆开检查。
一条几何定理从哪里来？ 它来自六类基础：对象定义、当前题设、体系公理、合法辅助构造、已经证明的定理，以及通用逻辑或代数变换。证明的任务，是把这些基础连接成一条不跳步、不循环并完整到达目标的推理链。
关键结论
- 定义说明对象含义，公理声明系统起点，定理是从这些起点推出的结论。
- 图形外观只能帮助提出猜想，不能自动成为证明前提。
- 辅助构造不是新增假设，而是依据允许的作图规则引入对象。
- 已证定理可以被封装复用，但调用时仍须满足全部前提。
- 第一性追溯应在需要诊断时展开，不必在每份证明中重复所有底层细节。
- 合法依赖必须有方向且无循环，不能用目标或其推论反证目标。
- 图谱展示来源，独立证明检验这些来源能否被主动调用。
第一性原理在几何中具体指什么？
第一性原理不是一句抽象口号，而是当前几何体系明确接受的基础对象、关系和推理规则。 不同体系可以选择不同起点，因此第一性不是“永远只有一组公理”，而是“在同一体系内公开起点并保持推导一致”。
欧几里得《几何原本》第一卷先列定义、公设与共同概念，再展开命题。1932 年，Birkhoff 在尺度与量角器公理体系中直接把距离和角度测量纳入基础。两者起点不同，却都体现同一方法：先声明可以依赖什么，再从中演绎。
几何中的基础可以分为六层：
| 层次 | 回答的问题 | 示例 |
|---|---|---|
| 定义 | 对象是什么意思？ | 中点意味着共线且两段等长 |
| 题设 | 当前问题给了什么？ | $AB=AC$、$DE\parallel BC$ |
| 公理 | 体系从哪里开始？ | 点线关系、距离与角度基础 |
| 构造 | 可以合法增加什么对象？ | 过点作平行线、连接两点 |
| 已证定理 | 哪些结论可复用？ | 内错角性质、AA 相似判定 |
| 逻辑与代数 | 怎样转换已有等式或命题？ | 等式相减、反证、分类讨论 |
定义、公理和定理为什么不能混在一起？
三者承担不同逻辑角色。 定义约定术语，公理作为体系起点，定理则需要证明；把它们混在一起，会让“为什么成立”失去边界。
例如“D 是 BC 的中点”不是一条额外神秘性质。按定义，它可以展开为 D 位于 BC 上且 $BD=DC$。而“对顶角相等”不是定义，因为对顶角的定义只说明两个角的位置关系；相等需要由邻补角与等式运算证明。
可以用一个简单判断：
- 如果一句话说明术语如何使用，它通常是定义；
- 如果一句话被体系明确接受而不在体系内证明，它是公理；
- 如果一句话需要从已有基础推出，它是定理。
案例一：对顶角相等究竟从哪里来？
对顶角相等不是从图形“看起来对称”得到，而是从两组邻补角等式中消去公共角。 这是一个短依赖链，适合观察第一性追溯。
两直线交于 O，形成角 $\angle AOC$ 与 $\angle BOD$。由邻补角关系：
$$ \angle AOC+\angle COB=180^\circ, $$
$$ \angle BOD+\angle COB=180^\circ. $$
两个等式右侧相同，并包含同一个 $\angle COB$。由等量减等量，得到：
$$ \angle AOC=\angle BOD. $$
这条证明可以拆成：
相反射线与平角定义
↓
两组邻补角和为 180°
↓ 等式相减
对顶角相等
图形帮助发现两组角，但等式关系和消去步骤才是证明依据。
案例二：勾股定理为什么不是一个孤立公式？
$a^2+b^2=c^2$ 是结论的代数表达，证明则需要把它接入相似、面积或其他更基础关系。 不同证明可以选择不同依赖，但每一条路线都必须公开中间桥梁。
数形智拍当前记录的一条路线，从直角三角形斜边上的高出发，得到两个小直角三角形与原三角形相似；由相似比例得到射影关系，再将两条等式相加推出勾股结论。
角与相似的基础
↓
AA 相似判定
↓
射影定理
↓
勾股定理
如果 AA 相似或射影关系尚未建立，直接背公式不会解释证明为何成立。这也是知识图谱比公式清单多出的信息：它显示结论背后的中间层。
辅助线是新增假设吗？
合法辅助线不是随意增加一个有利条件，而是依据构造规则引入新对象，再从定义和已有关系推出它的性质。 “过 A 作 BC 的平行线”可以引入平行关系；“随手画一条看似平行的线”则不能成为依据。
辅助构造通常完成三件事：
- 把分散条件装入同一个三角形或圆结构；
- 为目标定理补齐等角、等长、直角或比例前提；
- 将难以直接处理的目标转换为已经会证明的中间问题。
关于七类常见构造，可继续阅读《几何辅助线怎么找？》。
为什么第一性思考不等于每次都从零开始？
已经证明的定理可以作为可复用模块，第一性思考要求知道何时以及怎样拆开模块，而不是拒绝模块。 如果每次使用相似判定都从公理重证，证明会失去层次，认知资源也会被重复步骤占用。
合理做法是分两种场景：
| 场景 | 处理方式 |
|---|---|
| 正常解题 | 调用已掌握定理，并明确检查其前提 |
| 出现理解缺口 | 沿图谱展开该定理的来源，直到找到断点 |
这类似程序中的函数：平时通过接口复用，需要诊断时查看内部实现。定理的“接口”是前提和结论，证明是内部实现。
怎样逐层追溯一条定理？
追溯应从目标反向进行，同时在每一层保留证明方向。 可以采用下面六步：
- 写出目标定理的完整“若……则……”形式。
- 列出当前证明直接调用的前置定理。
- 检查每个前置的全部使用条件是否已成立。
- 对不理解的前置继续反向展开，而非展开全部节点。
- 到达公理、定义或已确认基础后停止。
- 再从基础向前重建一次，确认箭头方向没有颠倒。
反向追溯适合定位，正向重建适合验证。只反向查看容易产生“都认识”的熟悉感，只有再从基础推出目标，才能检查链条是否真正可调用。
数形智拍如何呈现定理来源？
数形智拍原理用定理节点、依赖边和标准证明共同表达来源。 当前图谱包含 4 个公理、138 条定理与 330 条依赖边，最大依赖深度为 16 层。
节点详情回答“这是什么”，入边回答“它依赖什么”，出边回答“它能用于哪里”，标准证明解释“每条边内部怎样成立”。独立证明入口则检验这些结构能否从空白状态重新构造。
可以在数形智拍原理图谱查看节点，或阅读《几何定理知识图谱》了解边的语义。
常见问题
第一性原理是不是等同于公理？
不完全等同。公理是形式体系中的基础命题；第一性思考还包括识别定义、题设、合法构造、通用逻辑，以及判断哪些已证定理可以作为当前模块调用。
一条定理必须只有一种来源吗？
不是。同一结论可以有多种证明，每种证明对应不同的前置集合。来源不是唯一的，但每条路线都必须合法、连续且无循环。
图上看起来明显的关系为什么还要证明？
示意图可能不按比例绘制，视觉外观只能提示猜想。除非题设、标记、定义或已有定理给出关系，否则“看起来等长或平行”不能成为证明依据。
追溯到公理就等于真正掌握吗？
不等于。追溯让来源可见，掌握还要求能够从基础向前独立重建，并在后续时段或变式中再次调用。
结语：让每一条结论都能回答“为什么”
第一性原理学习几何的价值，不是把所有证明写得更长，而是让结论随时可以被拆解：定义了什么、接受了什么、构造了什么、调用了什么，又怎样到达目标。
下一步可以在数形智拍图谱中任选一条熟悉定理，先沿入边追溯到基础，再关闭标准证明正向重建。若中途停止，停止的位置就是当前最具体的学习任务。
参考资料
- Euclid, Elements, Book I.
- Birkhoff, A Set of Postulates for Plane Geometry, Based on Scale and Protractor, 1932.
- Hilbert, The Foundations of Geometry, 1899.
- Avigad et al., Proof-checking Euclid, 2017.
- Institute of Education Sciences, Organizing Instruction and Study to Improve Student Learning.
- Karpicke & Blunt, Retrieval Practice Produces More Learning than Elaborative Studying with Concept Mapping, 2011.
- 数形智拍产品与原理图谱, ByuTech.