arXiv 研究：LLM 数学证明风格与人类不同，偏爱从头构建推理链
AI has its own style in mathematical proving
研究者让三个大模型重证了 Euclid《Elements》全部 465 个命题，再用网络分析对比引用结构。发现 AI 有 40% 引用指向定义和公设，人类只有 13%，AI 喜欢从零搭论证而不是引用成熟定理。做形式化验证或用模型辅助写数学论文的人都值得看看这套量化方法。
一项 arXiv 论文让三个大语言模型独立重新证明 Euclid《Elements》的全部 465 个命题，并用 Jaccard 相似度和复杂网络分析方法对比 AI 与人类证明的引用选择。
结果显示 AI 证明风格差异稳定且可复现：AI 各次运行之间的平均成对 Jaccard 相似度约为 0.68，而 AI 与人类证明之间仅约 0.37，前者接近后者的两倍。引用结构上，AI 约 40% 的引用指向基础元素（定义、公设、公理），人类证明只有 13%；即使引用定理，AI 也倾向引用更久远的结果，其多出的引用约一半来自人类证明的上游依赖。
论文将这种特征命名为"building from the ground up"，即 AI 倾向从基础元素自行搭建论证，而非直接引用更成熟的后续定理。这为理解 AI 生成证明为何难以解读提供了解释，也提示数学家在审阅 AI 证明时需关注其引用链条的组织方式。
AI has its own style in mathematical proving
As large language models increasingly generate mathematical proofs, whether they develop a proving style distinct from that of human mathematicians remains an open question. This question is particularly pressing as mathematicians increasingly voice concerns that proofs generated by large language models are difficult to interpret. Here we ask three large language models to independently reprove all 465 propositions of Euclid's \textit{Elements} and compare their citation choices against the human-proof baseline through Jaccard similarity and complex network analysis. We find that AI-generated proofs differ from human proofs, and this difference is stable and reproducible: mean pairwise Jaccard similarity among AI runs (~0.68) is nearly twice that between AI and human proofs (~0.37), and cross-run classification consistency is also high. By examining citation structure in detail, we identify the concrete signature of this difference: approximately 40% of AI citations point to foundational elements (definitions, common notions, and postulates), compared with only 13\% in human proofs; even among theorem-to-theorem citations, AI tends to cite more distant results. Roughly half of AI's extra citations trace to the upstream dependencies of the human proof. Together, these findings suggest that the AI proving style is a tendency to construct arguments on its own from foundational elements rather than directly citing later, more established results, which we term "building from the ground up". Our findings offer a new perspective on how AI systems organise and invoke mathematical knowledge, with implications for understanding the interpretability of AI-generated proofs.
This report is categorized under AITOP's "Papers" desk. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include arXiv, Euclid, Jaccard相似度, 可解释性.
Source attribution: curated from arXiv cs.AI (@Xiaokai Li, Ziyu Zhou, Qibin Cheng, Yangcheng Wu, An Zeng, Ying Fan).