allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/docs/research_stack_usage_graph.md
allaun 3b15d252f7 docs: add Research Stack searchable usage point graph 
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)
2026-06-21 06:39:39 -05:00

3.4 KiB
Raw Blame History

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

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.