mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3b15d252f7
Generate a unified entity/edge graph of Research Stack to support SilverSight porting decisions: - 13,296 entities: 849 Lean modules, 3,175 theorems, 7,784 defs, 215 scripts, 1,235 docs, services, databases, nodes, skills, goals - 13,913 edges: imports, contains, uses_service, touches_database, references_doc, runs_on, hosted_by - Math-kind classification, sorry/theorem/def counts, top in-degree modules - Neon service and database inventory - docs/generate_research_stack_usage_map.py for regeneration Build: 2978 jobs, 0 errors (lake build)
92 lines
3.4 KiB
Markdown
92 lines
3.4 KiB
Markdown
# Research Stack Searchable Usage Map
|
|
|
|
- **Entities:** 13296
|
|
- **Edges:** 13913
|
|
|
|
## Entity counts
|
|
- `def`: 7784
|
|
- `theorem`: 3175
|
|
- `doc`: 1235
|
|
- `module`: 849
|
|
- `script`: 215
|
|
- `mathlib`: 15
|
|
- `service`: 8
|
|
- `node`: 6
|
|
- `database`: 4
|
|
- `skill`: 3
|
|
- `goal`: 2
|
|
|
|
## Top modules by in-degree
|
|
- `FixedPoint` — imported by 97 modules
|
|
- `Bind` — imported by 18 modules
|
|
- `Mathlib.Data.Nat.Basic` — imported by 16 modules
|
|
- `Mathlib.Data.Real.Basic` — imported by 11 modules
|
|
- `PhysicsScalarBridge` — imported by 10 modules
|
|
- `ExtremeParameterTest` — imported by 9 modules
|
|
- `Mathlib` — imported by 7 modules
|
|
- `Mathlib.Tactic` — imported by 6 modules
|
|
- `ManifoldNetworking` — imported by 6 modules
|
|
- `Quaternion` — imported by 4 modules
|
|
- `Mathlib.Data.Finset.Basic` — imported by 4 modules
|
|
- `Mathlib.Data.Set.Basic` — imported by 4 modules
|
|
- `Atoms` — imported by 4 modules
|
|
- `PBACSSignal` — imported by 4 modules
|
|
- `Mathlib.Data.Fin.Basic` — imported by 3 modules
|
|
- `SSMS` — imported by 3 modules
|
|
- `Mathlib.Data.List.Basic` — imported by 3 modules
|
|
- `FAMM` — imported by 3 modules
|
|
- `Mathlib.Data.Int.Basic` — imported by 3 modules
|
|
- `Boundary` — imported by 3 modules
|
|
|
|
## Top theorem-producing modules
|
|
- `HamiltonianVerification` — theorems=324 defs=7 sorries=0 kind=quantum
|
|
- `i` — theorems=107 defs=7 sorries=0 kind=algebra
|
|
- `green_57` — theorems=69 defs=34 sorries=0 kind=algebra
|
|
- `i` — theorems=68 defs=1 sorries=0 kind=number_theory
|
|
- `SidonSets` — theorems=68 defs=17 sorries=0 kind=number_theory
|
|
- `DeltaGCLCompression` — theorems=62 defs=37 sorries=0 kind=algebra
|
|
- `FixedPoint` — theorems=62 defs=99 sorries=0 kind=fixedpoint
|
|
- `HamiltonianFormal` — theorems=61 defs=25 sorries=0 kind=quantum
|
|
- `E8Sidon` — theorems=60 defs=23 sorries=5 kind=number_theory
|
|
- `tenenbaum` — theorems=54 defs=8 sorries=0 kind=number_theory
|
|
- `bipartite_reconstruction` — theorems=52 defs=14 sorries=0 kind=algebra
|
|
- `erdos_846` — theorems=47 defs=5 sorries=0 kind=number_theory
|
|
- `erdos_152` — theorems=45 defs=7 sorries=0 kind=number_theory
|
|
- `Q16InverseProof` — theorems=44 defs=10 sorries=0 kind=fixedpoint
|
|
- `SpherionTwinPrime` — theorems=41 defs=28 sorries=0 kind=number_theory
|
|
- `Tests` — theorems=39 defs=20 sorries=0 kind=algebra
|
|
- `SpatialHashCodec` — theorems=36 defs=19 sorries=0 kind=rrc
|
|
- `DomainDetector` — theorems=31 defs=7 sorries=0 kind=rrc
|
|
- `graph_conjecture2` — theorems=30 defs=2 sorries=0 kind=algebra
|
|
- `ii` — theorems=28 defs=3 sorries=0 kind=number_theory
|
|
|
|
## Math-kind distribution
|
|
- `fixedpoint`: 429
|
|
- `algebra`: 132
|
|
- `avm`: 51
|
|
- `quantum`: 50
|
|
- `braid`: 36
|
|
- `routing`: 33
|
|
- `geometry`: 33
|
|
- `rrc`: 31
|
|
- `number_theory`: 31
|
|
- `general`: 15
|
|
- `analysis`: 8
|
|
|
|
## Neon-hosted services
|
|
- **PostgreSQL on neon** — arxiv-pg
|
|
- **Ollama on neon** — http://100.92.88.64:11434 DeepSeek-Prover,Goedel-Prover,Qwen,hermes3
|
|
- **Vikunja on neon** — http://100.92.88.64:3456
|
|
- **Headroom proxy on neon** — http://100.92.88.64:8787
|
|
|
|
## Databases on neon
|
|
- **arxiv** — arxiv_papers,arxiv_paper_codes8,citations
|
|
- **ene** — ENE graph schema
|
|
- **appflowy** —
|
|
- **vikunja** —
|
|
|
|
## How to use this graph
|
|
- Load `research_stack_usage_graph.json` into any search/index tool.
|
|
- Render the DOT with: `dot -Tsvg research_stack_usage_graph.dot -o graph.svg`
|
|
- Query examples: find modules with `math_kind=braid` and `sorry_count>0`;
|
|
find scripts that touch `db:arxiv`; find docs referenced by a script.
|