Astrolabe: A Content-Addressable Hypergraph for Semantic Knowledge Management
Dependency graphs for Lean formalization projects, such as leanblueprint graphs and declaration-level graphs, label every edge only as "uses". They do not record how a dependency is used (unfold, rewrite, apply), which limits knowledge management and autoformalization agents.
Astrolabe is a content-addressable hypergraph. Each entry (nerve) is identified by the SHA-256 hash of its record, has an ordered reference list of arbitrary width, and carries an opaque record string interpreted by plugins. The store admits decompositions by width and by depth. The LeanNets plugin stores LaTeX and Lean 4 statements and proofs as entries, splitting Lean theorem declarations into a statement entry and a proof entry, and extracts formal dependencies from Lean compilation artifacts into a directed semantic network.
A prototype stored as a single JSON file shows informal theorems such as Heine-Borel linked to Lean declarations such as IsCompact.isClosed, with semantic edge records. Future work proposes network analysis of the store to improve premise retrieval for autoformalization.
| Edge sort pair | Meaning |
|---|---|
| (theorem, proof) | Statement–proof link |
| (theorem, definition) | Depends on definition |
| (proof, lemma) | Proof cites lemma |
| (theorem, theorem) | Cross-source correspondence |