用公理向量结构化数学定理,实现逻辑关系的量化分析与可视化。
The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
- 将定理表示为公理索引的证明向量,构建逻辑依赖的结构化模型。
- 通过余弦距离等指标量化定理间相似性,支持向量聚类与热图可视化。
- 集成AI助手可理解自然语言定理并推测证明路径,适合形式化验证与教育应用。
Axiom-Based Atlas 是一种新框架,将数学定理结构化表示为基于基础公理系统(如希尔伯特几何、皮亚诺算术、ZFC)的证明向量。通过将定理的逻辑依赖映射到以公理为索引的向量空间,该框架提供了一种可视化、比较和分析数学知识的新方式。这一向量形式不仅捕捉定理的逻辑根基,还支持定量相似性度量(如余弦距离),为结构性比较提供新分析层。结合热图、向量聚类与AI辅助建模,该地图可按逻辑结构而非数学领域对定理进行分组。我们还推出了原型助手Atlas-GPT,能解析自然语言定理并建议可能的证明向量,支持自动化推理、数学教育与形式化验证。该方向部分受陶哲轩近期关于符号与结构数学融合的启发。Axiom-Based Atlas旨在构建一个可扩展、可解释、人类可读且适配人工智能的数学推理模型,推动未来形式化数学系统的发展。
原文摘要 · Abstract (English)
The Axiom-Based Atlas is a novel framework that structurally represents mathematical theorems as proof vectors over foundational axiom systems. By mapping the logical dependencies of theorems onto vectors indexed by axioms - such as those from Hilbert geometry, Peano arithmetic, or ZFC - we offer a new way to visualize, compare, and analyze mathematical knowledge. This vector-based formalism not only captures the logical foundation of theorems but also enables quantitative similarity metrics - such as cosine distance - between mathematical results, offering a new analytic layer for structural comparison. Using heatmaps, vector clustering, and AI-assisted modeling, this atlas enables the grouping of theorems by logical structure, not just by mathematical domain. We also introduce a prototype assistant (Atlas-GPT) that interprets natural language theorems and suggests likely proof vectors, supporting future applications in automated reasoning, mathematical education, and formal verification. This direction is partially inspired by Terence Tao's recent reflections on the convergence of symbolic and structural mathematics. The Axiom-Based Atlas aims to provide a scalable, interpretable model of mathematical reasoning that is both human-readable and AI-compatible, contributing to the future landscape of formal mathematical systems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。