LLM2D
基于公理的图集:通过基础证明向量的定理结构映射
The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
作者: Harim Yoo
发布日期: 4/2/2025
arXiv ID: oai:arXiv.org:2504.00063v1

摘要

arXiv:2504.00063v1 宣告类型: 新 摘要: 基于公理的图集是一种新的框架,它以证明矢量的形式结构化地表示数学定理,基于基础公理系统。通过将定理的逻辑依赖关系映射到按公理索引的矢量上——例如希尔伯特几何、皮亚诺算术或ZF(C)——我们提供了一种新的方式来可视化、比较和分析数学知识。这种基于矢量的形式主义不仅捕捉了定理的逻辑基础,还使得能够使用诸如余弦距离等定量相似度度量来比较数学结果,从而为结构性比较提供了一种新的分析层。借助热图、矢量聚类和AI辅助建模,这种图集不仅可以通过逻辑结构对定理进行分组,还可以通过数学领域进行分组。我们还提出了一种原型助手(Atlas-GPT),它可以解释自然语言定理并建议可能的证明矢量,支持未来在自动推理、数学教育和形式验证方面的应用。 这一方向部分受到了陶哲轩近期关于象征性数学与结构性数学趋同的反思的启发。基于公理的图集旨在提供一种可扩展、可解释的数学推理模型,既易于人类阅读又兼容AI,从而为未来的正式数学系统景观做出贡献。