Scholia DSH 插件
Scholia 是一款针对 Lean 4 / Mathlib 的插件，旨在解决定理依赖锥（可能多达 1829 个模块）阅读困难的问题。它通过算法将复杂的依赖关系简化为一条可读的主线，并将定理渲染为论文风格页面。 该插件支持生成包含数学公式、源码、分步标注、阅读大纲、步骤页面以及模块级依赖图（DAG）的静态页面。目前版本为 v0.1，依赖 Node.js 24+ 和 SQLite，需配合外部 Corpus 数据使用。
Read Moredsh-tool-strict-check: Validating Code and Commands with a Real Compiler
`dsh-tool-strict-check` is a host plugin for DeepSeek Harness (DSH) designed to fix mechanical errors by replacing subjective agent judgment with real compiler checkers (such as the Lean 4 kernel and dangerous Shell rules). Located in the `admin-security` category, it provides four checking modes: `status`, `lean` (runs Lean 4 and disallows `sorry`), `batch` (compiler syntax checking), and `commands` (Shell static rules). Installation requires adding the plugin to the DSH profile and installing the Lean 4 toolchain as needed. It validates code by enforcing strict compilation rules, but does not support
Read More