scholia 怎么安装？

在已安装 dsh CLI 引擎的环境中，进入插件页复制安装命令一键执行即可；尚未跑自动兼容性验证，可查看页面内的依赖与入口分析。

scholia 兼容性怎么样？

尚未跑自动兼容性验证，可查看页面内的依赖与入口分析。

scholia 有中文文档吗？

已提供中文翻译 README（由 DeepSeek 最新模型翻译生成），本站可切换中英文对照阅读。

scholia 还在维护吗？

GitHub 0 星。最近一次上游提交在 2026/10/8。

定理论文视图 H2CO3w/scholia

DeepSeek Harness

H2CO3w26 天前有提交已提供中文文档扫描：含敏感能力

在 GitHub 查看 ↗

把 Lean 定理渲染成论文页并提炼证明主线

29.9/100

综合分

GitHub 星标

—

npm 周下载

—/5

用户评分

数据截至 2026/10/8 · 周下载取自 npm 全网（含 CI / 镜像），非本站安装数；综合分由星标、活跃度与兼容性检查合成。

安装命令 · 需先装 dsh CLI 引擎

dsh plugin --profile web add H2CO3w/scholia

该包不可直接 npm 安装，改从 GitHub 源安装（明细见下方安装检查）

状态速览

判定依据：实装验证 · 静态安装检查 · 自动扫描 · 仓库维护状态

信任档位：需留意

是什么

dsh 原生插件 · tool

装得上吗

实装验证未通过（unknown），装前请到仓库确认最近更新与 issue

L4 · 真实安装等级说明 →

安全吗

本站尚未对该插件做风险分级

暂未覆盖，不等同于无风险

还在维护吗

活跃：最近一次提交在 26 天前

档位由哪些信号合成

本站实装验证（真实安装 L4 覆盖全站；L5 为运行时冒烟或实机截图，覆盖范围小于 L4） · 验证所用 dsh 版本 · 静态安装检查 · 风险分级 · 仓库维护状态。下方各区块是它的证据明细。

验证判据与等级说明 →

⚠︎ 实装验证未通过（unknown · 2026/10/9） ——可能是验证环境差异，装前建议到 GitHub 仓库确认最近更新与 issue。

社区实装还没有人打卡 · 装过的第一个就是你

安全扫描自动 · 静态分析源码

v2.7.0

🔵 扫描：含敏感能力尚无人工评估

展开查看扫描说明与证据 ↓

静态扫描发现插件具备触达本地系统的能力：执行外部命令、读写/删除本地文件、读取剪贴板或密钥类环境变量（至少其一）。这是能力清单，不是危险判定——具体能力项与证据见下方，安装前请自行判断是否需要。

读写/删除本地文件发起外部网络请求

查看扫描证据（共 45 处，展示前 24 条）

写入本地文件
src/tools/ledger-export.mjs:89
await mkdir(fontDir, { recursive: true })
写入本地文件
src/tools/ledger-export.mjs:91
await writeFile(path.join(assetDir, filename), text, 'utf8')
写入本地文件
src/tools/ledger-export.mjs:96
await copyFile(path.join(vendorDir, filename), target)
读取本地文件
src/tools/ledger-export.mjs:101
const entries = await readdir(sourceDir, { withFileTypes: true })
写入本地文件
src/tools/ledger-export.mjs:105
await copyFile(path.join(sourceDir, entry.name), path.join(assetDir, target, entry.name))
写入本地文件
src/io/artifacts.mjs:135
await mkdir(dirname(file), { recursive: true })
写入本地文件
src/io/artifacts.mjs:138
await writeFile(tmp, text, 'utf8')
写入本地文件
src/io/artifacts.mjs:139
await rename(tmp, file)
删除本地文件
src/io/artifacts.mjs:142
await rm(tmp, { force: true })
读取本地文件
src/io/artifacts.mjs:161
text = await readFile(file, 'utf8')
读取本地文件
src/io/index-db.mjs:39
if (!existsSync(dbPath)) return null
读取本地文件
src/io/index-db.mjs:41
if (statSync(dbPath).size === 0) return null
读取本地文件
src/io/index-db.mjs:89
if (!existsSync(corpusPath)) {
写入本地文件
src/io/index-db.mjs:96
mkdirSync(dirname(dbPath), { recursive: true })
写入本地文件
src/io/index-db.mjs:129
renameSync(tmpPath, dbPath)
删除本地文件
src/io/index-db.mjs:139
rmSync(`${tmpPath}${suffix}`, { force: true })
读取本地文件
src/io/index-db.mjs:175
if (!existsSync(dbPath)) {
读取本地文件
src/io/corpus.mjs:37
const stream = createReadStream(corpusPath, { encoding: 'utf8' })
发起网络请求
vendor/katex/katex.mjs:7516
var next = parser.fetch().text;
发起网络请求
vendor/katex/katex.mjs:7945
var token = parser.fetch();
发起网络请求
vendor/katex/katex.mjs:9494
var nxt = parser.fetch().text;
发起网络请求
vendor/katex/katex.mjs:9499
nxt = parser.fetch().text;
发起网络请求
vendor/katex/katex.mjs:9505
nxt = parser.fetch().text;
发起网络请求
vendor/katex/katex.mjs:9613
var next = parser.fetch().text;

扫描于 2026/11/4（0 天前） · 范围入口闭包 + 发布文件清单 · 来源 GitHub 仓库

静态扫描只反映源码中出现的调用，不构成安全背书；人工评估与自动扫描相互独立、互不覆盖。

给这个插件打分还没有人投票↓

用户评分

还没有人投票，来当第一个

广告精选好物

飞利浦 TAH6519 主动降噪耳机 ¥299

头戴式无线 anc 主动降噪，蓝牙连接，久戴舒适向。

·anc 主动降噪 · 头戴式无线
·价格与库存以商品页实时为准

去淘宝看看→

广告MCP 兼容手册

装完插件，给 AI 接上 MCP

Cursor、Claude Code、VS Code 逐个核对：能不能装、配置怎么写、装不上是什么原因。

·按客户端逐格核对
·结论标注依据与风险等级

查 MCP 兼容性→

功能亮点

渲染定理为论文页
提炼证明主线

形式化证明编译器能读，数学家读不了。这个 DSH 插件把 Lean 4 / Mathlib 定理渲染成论文页面，并把 1,829 个模块的依赖锥收敛成一条可读主线。形式化证明 → 可读论文。

README

由 DeepSeek 最新模型翻译生成

scholia （包名 dsh-scholia） v0.1 —— 早期且不完整。接口还会变。一个 DSH 插件，把形式化的定理（Lean 4 / Mathlib）变成数学家真正读得进去的东西：一张论文风格的页面，陈述用数学排版渲染，附证明提纲，还有锚定到形式化对象的注释。这里的一切都来自真实语料：Mathlib 声明，加上语料之外的 Lean 源码，用作回归测试夹具。产出什么 | 产物 | 是什么 | | 论文视图 out/render/.html | 每个定理一页：渲染后的陈述、Lean 源码、逐步骤注释。零。 | | 主线提纲 out/outline/<root>/index.html | 把证明的依赖锥压缩成一条有序的步骤线，每一步都带作者自己写的一句话摘要。 | | 步骤页 out/outline/<root>/NN.html | 针对某一步：它带进来的模块，每个模块各有自己的摘要。 | | 依赖图 out/graph/.svg | 模块级 import DAG，静态渲染。 | 先从 out/outline/Euler.Solution/index.html 和 out/render/CHSH_inequality_of_comm.html 看起。提纲是怎么搭出来的光看模块图，1829 个节点，根本读不下去。

展开完整文档（README 剩余 1 节）

scholia

（包名 dsh-scholia）

v0.1 —— 早期且不完整。接口还会变。

一个 DSH 插件，把形式化的定理（Lean 4 / Mathlib）变成数学家真正读得进去的东西：一张论文风格的页面，陈述用数学排版渲染，附证明提纲，还有锚定到形式化对象的注释。

这里的一切都来自真实语料：Mathlib 声明，加上语料之外的 Lean 源码，用作回归测试夹具。

产出什么

| 产物 | 是什么 |
| 论文视图 out/render/.html | 每个定理一页：渲染后的陈述、Lean 源码、逐步骤注释。零 。 |
| 主线提纲 out/outline/<root>/index.html | 把证明的依赖锥压缩成一条有序的步骤线，每一步都带作者自己写的一句话摘要。 |
| 步骤页 out/outline/<root>/NN.html | 针对某一步：它带进来的模块，每个模块各有自己的摘要。 |
| 依赖图 out/graph/.svg | 模块级 import DAG，静态渲染。 |

先从 out/outline/Euler.Solution/index.html 和 out/render/CHSH_inequality_of_comm.html 看起。

提纲是怎么搭出来的

光看模块图，1829 个节点，根本读不下去。真正管用的是主线：

- 从声明论文定理的那个模块出发（取自源码仓库的 formalization.yaml）；
- 每一步都沿着子树最大的那条依赖走；
- 每一步的载入量是望远镜式差值
|subtree(p_i)| - |subtree(p_{i+1})|，它把依赖锥精确划分开——
不重叠，也不遗漏。

每个模块都带一段 /-! ... -/ 文档字符串，由写文件的人自己写，所以每一步都能贴上一句数学描述，而不是文件名。

阅读顺序是基础优先（--order reading）；反过来就是原始依赖顺序。

目录结构

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+（用到内置的 node:sqlite）；想重新生成图/提纲产物，还需要 Lean 4 源码。

语料（data/lsv2.jsonl）和词典索引（cache/lexicon.db）不在本仓库里——它们有几百 MB。见 docs/USAGE.md。

状态

- 360 个测试，0 失败。
- 论文视图是成熟的部分；提纲和图较新（v1.4）。
已知限制记录在 docs/ARCHITECTURE.md §11，包括 Unicode→LaTeX 的缺口、骨架提取器对表层语法的依赖，以及 v1.3 的「签名未知」处理覆盖了哪些情况。

License

MIT — 见 LICENSE。

随附的第三方材料保留自己的许可证：

- vendor/katex/ — KaTeX，MIT（见 vendor/katex/LICENSE 和 PROVENANCE.json）
- test/fixtures/lean/ — 片段来自 openai/NavierStokesAndEuler， Apache-2.0，出处标注在每个 fixture 头部