前言¶
在 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 倉庫
