The Axiom-Based Atlas: A Structural Mapping of Theorems via Foundational Proof Vectors
Harim Yoo
TL;DR
The paper tackles the challenge of structurally comparing theorems across different foundational systems by encoding proofs as axiom-based vectors, enabling visualization, clustering, and quantitative similarity analyses. The authors propose a vector-based formalism with coordinates tied to axioms from systems such as Hilbert geometry, Peano arithmetic, and ZFC, and they leverage heatmaps, cosine similarity, and cross-system vector concatenation to reveal structural relationships. A key contribution is the Atlas-GPT prototype, which semantically parses natural-language theorems to predict likely proof vectors and provides explanations, illustrating a pathway toward AI-assisted formal reasoning and education. This framework promises scalable, interpretable mappings of mathematical knowledge that can support automated reasoning, curriculum design, and integration with proof assistants, ultimately bridging symbolic logic with data-driven analytics. The underlying idea is captured by the relation cosines between proof vectors $v$ and $w$, with cosine similarity $ rac{v \
Abstract
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.