Update graph based on the latest mathlib and Implement a 3D version of math kingdom#14
Open
lhyundeadsoul wants to merge 5 commits into
Open
Update graph based on the latest mathlib and Implement a 3D version of math kingdom#14lhyundeadsoul wants to merge 5 commits into
lhyundeadsoul wants to merge 5 commits into
Conversation
add gragh data generation script
Regenerate release/data/import_graph.txt from the current mathlib4
(v4.32.0-rc1), growing from 3763 to 8244 modules. The newer
`lake exe graph` export emits isolated-node declaration lines
("X" [shape=ellipse];) for sink nodes, which the old parser choked on;
gen_graph.py now handles both line forms.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
New, independent data pipeline (kingdom/regions.yaml, kingdom/tier_overrides.yaml, script/gen_kingdom.py) that maps mathlib4's import graph onto mountains (topic regions) with two elevation scales: a heuristic macro_tier approximating abstraction level within a region (unification breadth + reverse PageRank, quantile-binned, with a manual override file for later curation), and micro_elevation for local dependency depth. Category theory is modeled as a shared summit layer floating above the other mountains. Regions are laid out with a golden-angle spiral packing so mountains never overlap. Full format documented in kingdom/schema.md, including known heuristic limitations. Output data lives in kingdom/data/kingdom_data.json and is fully decoupled from any renderer. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
gen_kingdom.py now pulls each module's own /-! ... -/ doc-string straight out of the local mathlib4 checkout (title + intro paragraph, truncated), plus a deterministic mathlib4_docs URL. 96% of the 8244 nodes get a title, 83% get a summary; both are real source content, not generated. Documented in kingdom/schema.md. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
kingdom/viewer/index.html is a single self-contained page (Three.js and the full kingdom dataset inlined, no network access needed) rendering the mountains as a progressively-disclosed 3D scene: collapsed tier platforms by default, click-to-expand detail, search, and a click-to- highlight explorer for a concept's direct dependencies. Replaces the separate per-folder run.sh/run.bat (which was a source of confusion -- easy to launch the wrong one) with a single pair of scripts at the repo root that take a 2d/3d argument and dispatch to either the bgfx explorer or the 3D viewer, opening the latter in an app-mode browser window when Edge/Chrome is available. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Author
|
This is the final result. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
inspired by your 2D implementation, did a 3D verison to immerse yourself into the math kingdom.
the Z-axis is design to represent the abstract level of a concept.