Scholia DSH 插件
Scholia 是一款针对 Lean 4 / Mathlib 的插件，旨在解决定理依赖锥（可能多达 1829 个模块）阅读困难的问题。它通过算法将复杂的依赖关系简化为一条可读的主线，并将定理渲染为论文风格页面。 该插件支持生成包含数学公式、源码、分步标注、阅读大纲、步骤页面以及模块级依赖图（DAG）的静态页面。目前版本为 v0.1，依赖 Node.js 24+ 和 SQLite，需配合外部 Corpus 数据使用。
阅读全文dsh-tool-strict-check: 用真实编译器校验代码与命令
`dsh-tool-strict-check` 是一个用于 DeepSeek Harness (DSH) 的主机插件，旨在通过引入真实的编译器检查器（如 Lean 4 内核、Shell 危险规则）来替代智能体主观判断，从而修复其机械性错误。 该插件位于 `admin-security` 类别，提供四种检查模式：`status`、`lean`（运行 Lean 4 并禁止 `sorry`）、`batch`（编译器语法检查）和 `commands`（Shell 静态规则）。安装需将插件添加至 DSH profile，并按需安装 Lean 4 工具链。它通过强制执行严格的编译规则来验证代码，但不支持
阅读全文