dsh-scholia
DSH 插件 dsh-scholia
插件会安装到这里；不确定时保持 web。
npx -y @deepseek-ai/dsh plugin --profile web add github:H2CO3w/scholia#5e206a656324a50ab48715833d6d8dfe81ac2bc7
DSH 插件 dsh-scholia
Scholia 以 dsh-scholia 发布，当前版本为 0.1.0。Plugin Hub 会校验它的 manifest，并保存精确安装来源，便于复现安装结果。
(package name dsh-scholia)
v0.1 — early and incomplete. Interfaces will change.
A DSH plugin that turns a formalized theorem (Lean 4 / Mathlib) into something a mathematician can actually read: a paper-style page with the statement rendered as math, a proof outline, and annotations anchored to the formal objects.
Everything here is generated from a real corpus of Mathlib declarations plus out-of-corpus Lean sources used as regression fixtures.
| Artifact | What it is |
|---|---|
Paper view out/render/*.html | One page per theorem: rendered statement, Lean source, per-step annotations. Zero <script>. |
Main-line outline out/outline/<root>/index.html | The proof's dependency cone reduced to a single ordered line of steps, each with the author's own one-sentence summary. |
Step pages out/outline/<root>/NN.html | For one step: the modules it brings with it, each with its own summary. |
Dependency graph out/graph/*.svg | The module-level import DAG, statically rendered. |
Start with out/outline/Euler.Solution/index.html and out/render/CHSH_inequality_of_comm.html.
The module graph alone is unreadable at 1829 nodes. What works is a main line:
formalization.yaml);|subtree(p_i)| - |subtree(p_{i+1})|, which partitions the cone exactly —
no overlaps, nothing missed.Every module carries a /-! ... -/ docstring written by whoever wrote the file,
so each step can be labelled with a sentence of mathematics instead of a file name.
Reading order is foundations-first (--order reading); the reverse is the raw
dependency order.
src/core/ pure logic: skeleton extraction, anchors, graph, validation
src/io/ corpus streaming, SQLite lexicon index, artifacts, contract
src/render/ pure string generation: paper view, outline, graph, math
src/tools/ the DSH tools
scripts/ offline export scripts
vendor/katex/ vendored KaTeX (self-contained, server-side rendering)
docs/ SPEC / ARCHITECTURE / INTERFACES / USAGE (Chinese)
test/ incl. out-of-corpus Lean fixtures
out/ generated artifacts
Node.js 24+ (uses the built-in node:sqlite), Lean 4 sources if you want to
regenerate the graph/outline artifacts.
The corpus (data/lsv2.jsonl) and the lexicon index (cache/lexicon.db) are
not in this repo — they are hundreds of MB. See docs/USAGE.md.
docs/ARCHITECTURE.md §11, including the
Unicode→LaTeX gaps, the surface-syntax dependence of the skeleton extractor,
and what the v1.3 "signature unknown" handling covers.MIT — see LICENSE.
Bundled third-party material keeps its own license:
vendor/katex/ — KaTeX, MIT (see vendor/katex/LICENSE and PROVENANCE.json)test/fixtures/lean/ — fragments from
openai/NavierStokesAndEuler,
Apache-2.0, attributed in each fixture header