前言¶
在 Lean 4 / Mathlib 的开发与阅读中，一个定理往往依赖着庞大的模块集合，依赖锥可能包含 1829 个模块。直接阅读如此复杂的依赖关系非常困难。Scholia 旨在解决这一问题，通过算法将庞大的依赖锥简化为一条可读的主线，并将形式化的定理转化为数学家可读的论文风格页面。
插件介绍¶
- 名称：
h2co3w/scholia（包名dsh-scholia） - 维护者：H2CO3w
- 核心价值：将 Lean 4 / Mathlib 定理渲染为论文风格页面，并减少其 1829 模块依赖锥为一条可读的主线。
核心功能¶
- 论文视图渲染：将 Lean 4 / Mathlib 定理渲染为论文页面，包含渲染后的数学公式、Lean 源码以及分步的标注。
- 生成主线大纲：通过算法提取依赖锥的主线，将原本难以阅读的模块依赖关系压缩为一条有序的阅读步骤，每一步都有作者撰写的摘要。
- 步骤页面与依赖图：生成具体的步骤页面，展示每一步引入的模块及其摘要；同时生成静态渲染的模块级依赖图（DAG）。
技术要求与环境¶
- 运行环境：使用 Node.js 24+ 和 SQLite。
- 测试状态：360 测试通过。
典型用法¶
插件生成的产物位于 out 目录下，包含以下部分：
- Paper view：
out/render/*.html。每个定理一个页面，包含渲染后的公式、源码和标注，无脚本标签。 - Main-line outline：
out/outline/<root>/index.html。 proof 的依赖锥主线。 - Step pages：
out/outline/<root>/NN.html。单个步骤的详细页面。 - Dependency graph：
out/graph/*.svg。模块级导入 DAG 的静态渲染。
在使用时，可以使用 --order reading 参数来指定从基础开始构建阅读顺序。示例入口文件包括 out/outline/Euler.Solution/index.html 和 out/render/CHSH_inequality_of_comm.html。
注意事项与限制¶
- 早期版本：当前版本为 v0.1，属于早期且不完整的版本，接口可能会改变。
- 数据依赖：仓库不包含 Corpus (
data/lsv2.l) 和 Lexicon DB (cache/lexicon.db)，这些文件不在仓库中。 - 已知限制：存在 Unicode→LaTeX 的转换间隙，且对表面语法有一定依赖性。
- 第三方库：插件集成了 KaTeX (MIT) 和 Lean fixtures (Apache-2.0)。
安装与生态¶
- 目录地址：SkillHub 插件目录
- 源码地址：GitHub 仓库
