AI 证明有自己的风格：重证《几何原本》465 条命题，引用相似度 0.68 远高于人机之间的 0.37
核心概要
三个大语言模型独立重证欧几里得《几何原本》全部 465 条命题，其引用选择与希思的人类证明基线系统不同。三次 Claude Opus 4.6 运行之间的平均成对 Jaccard 相似度为 0.68，而 AI 与人类证明之间仅 0.37，说明这种差异稳定可复现。差异的具体特征是 AI 约 40% 的引用指向定义、公理和公设等基础元素，人类证明中这一比例只有 13%。
深度剖析
大语言模型在数学证明中形成了可识别的自身引用风格，与人类数学家的证明选择系统不同。 此前对 AI 与人类证明差异的观察停留在冗长、纠缠局部细节、偏好程序化策略等表现层面，未回答这些表现是否反映 AI 调用数学知识的稳定规律。 三次 Claude Opus 4.6 独立运行之间的平均成对 Jaccard 相似度为 0.68，接近 AI 与人类证明之间 0.37 的两倍；同一命题在三次运行中被分到同一类别的比例整体为 69.5%。
这种风格的核心是从基础元素自下而上重建论证，而不是直接引用更晚、更成熟的结论。 人类证明网络中 86.8% 的引用指向定理，定义、公理和公设合计只占 13.2%；AI 证明中定理引用降到约 60%，三类基础元素合计约 40%。 在 Opus 证明中，引用距离均值为 111.2、中位数 61，人类证明分别为 86.3 和 38；仅保留定理间引用后 AI 的引用距离仍更长，Fable 5.1 与 GPT-6 Astra 的结果与 Opus 一致。
AI 多出来的引用大多落在人类证明的上游依赖中，说明双方常沿同一逻辑结构在不同层级进入。 在路径不同的 D 类命题上，AI 独有引用与人类独有引用被分开考察，以判断 AI 是否只是重复推导成熟结论的步骤。 D 类命题中 AI 独有引用平均有 47.0% 出现在人类证明引用的祖先集合里，若只计人类独有引用的祖先则为 34.5%；Fable 5.1 对应 52.7% 和 42.7%，GPT-6 Astra 对应 48.2% 和 39.0%。
启示与展望
结论的适用范围是欧几里得《几何原本》的 465 条命题、以希思英译证明为人类基线、且证明以自然语言书写；形式化证明不在考察范围内。
改变提示方式对自下而上倾向影响很小，但微调、在训练目标中加入引用偏好或改造证明生成流程能否引导这一风格，仍需进一步实验确定；Fable 5.1 的路径差异比例结果因该类证明仅 34 条而未能呈现统计上可靠的规律。