Skip to content

README.md

Latest commit

 

History

History
121 lines (88 loc) · 3.94 KB

README.md

File metadata and controls

121 lines (88 loc) · 3.94 KB

LeanNets Plugin

Transforms astrolabe.json into a directed network for graph analysis.

Architecture

Layer Components
Data astrolabe.json — entries with ref and record
Backend graph_builder · degree · centrality · dag · community · cluster
API GET /api/plugins/leannets/graph?size=&color=&cluster=
Network d3-force simulation + cluster attraction force
Color entryColor.ts → EntryBlock · EntryLink · EntryDetail

Data Model

Each entry: { "ref": [...], "record": "<JSON>" }

  • Atoms (degree 0): ref = [self_hash] → nodes
  • Edges (degree 1): ref = [A, B] → directed edge A → B
  • Hash: SHA256(ref₁ ‖ 0x00 ‖ ref₂ ‖ ... ‖ record)[:12 hex]

Record Convention

Two required fields for every atom:

Field Values
sort definition · theorem · lemma · proposition · corollary · proof · instance · citation
source tex · lean · bib (future: rocq · agda · hm)

Optional fields by source:

Field Source Description
title all Display name
notes tex lean Natural language, may contain $LaTeX$ and \\entryref{hash}{text}
content lean Source code (type signature or tactic body)
state lean proven or sorry
key bib Citation identifier

Source: tex

Sort derived from LaTeX environment: \\begin{theorem} → sort: "theorem"

{ "sort": "theorem", "source": "tex", "title": "...", "notes": "..." }
{ "sort": "proof", "source": "tex", "notes": "..." }

Source: lean

Sort derived from declaration keyword: def → definition, theorem → theorem

{ "sort": "theorem", "source": "lean", "title": "...", "state": "proven", "content": "..." }
{ "sort": "proof", "source": "lean", "title": "... (proof)", "content": "..." }

Source: bib

{ "sort": "citation", "source": "bib", "key": "...", "notes": "..." }

Edges

Sort is auto-derived: (sort_A, sort_B)

Edge Meaning
(theorem, proof) Statement ↔ proof
(theorem, definition) Depends on definition
(proof, lemma) Proof cites lemma
(theorem, theorem) Cross-source correspondence

Network Analysis

Size — node radius $r_v$

Metric Formula
uniform $r_v = c$
degree $r_v \propto \deg^+(v) + \deg^-(v)$
in-degree $r_v \propto \deg^-(v)$
out-degree $r_v \propto \deg^+(v)$
pagerank $\pi = \alpha M \pi + \frac{1-\alpha}{n}\mathbf{1}$
betweenness $c_B(v) = \sum_{s \neq v \neq t} \frac{\sigma_{st}(v)}{\sigma_{st}}$
katz $c_K(v) = \sum_{k=1}^{\infty} \alpha^k (A^k \mathbf{1})_v$
hub $\mathbf{h} = A\mathbf{a},\; \mathbf{a} = A^\top \mathbf{h}$
authority $\mathbf{a} = A^\top \mathbf{h},\; \mathbf{h} = A\mathbf{a}$
depth $d(v) = \max_r \text{longest-path}(r, v)$
reachability $\lvert\{u : v \rightsquigarrow u\}\rvert$

Color — node color

Mode Method
sort $\text{hue} = \text{hash}(\text{sort}) \bmod 360$
community Greedy modularity maximization
layer $\text{color} = \text{gradient}(d(v) / d_{\max})$
pagerank $\text{color} = \text{gradient}(\pi_v / \pi_{\max})$
spectral Communities from eigenvectors of $L = D - A$
curvature $\text{gradient}(c_B(v) / c_{B,\max})$

Colors propagate to: nodes, entry blocks, entry links, detail panel.

Cluster — node grouping

Method Algorithm
louvain Greedy modularity
sort Partition by sort
stage Partition by depth
spectral $k$-means on eigenvectors of $L$, $k$ from eigengap

Cluster force: $\mathbf{f}v = s \cdot \alpha \cdot (\mathbf{c}{k(v)} - \mathbf{x}_v)$ where $s \in [0,1]$ is tightness.