scholia

形式化定理写在 Lean 4 与 Mathlib 里，对习惯读论文的数学家往往晦涩难懂：陈述藏在源码里，依赖图动辄上千节点，很难看出「证明到底在干什么」。scholia 是面向这一痛点的 DSH 插件，把仓库里已形式化的定理转成可浏览的论文式页面，让陈述以数学公式呈现，并附上证明提纲与锚定在形式对象上的注释。

插件从真实 Mathlib 声明语料与回归用例出发生成多种产物：每个定理一张 Paper view（陈述、Lean 源码与分步注释）、将依赖锥压缩为有序「主线」的提纲索引与逐步页面，以及模块级 import 的静态依赖图。主线并非简单罗列 import，而是从声明定理的模块起，每步沿子树最大的依赖前进，并用各模块文档串中的数学句子作步骤摘要，阅读顺序还可按「先基础后结论」排列。

适合参与或跟进 Lean 形式化项目的人：想向合作者或自己快速复述一条定理在证明链上的位置、需要把形式化成果当成可读文稿审阅，或要在庞大模块图中抓住一条清晰叙事线时，scholia 能把形式世界和论文式阅读体验拉近。项目仍处于早期（v0.1），界面与能力会继续变化，Paper view 相对成熟，提纲与图较新，已知限制见项目文档。

若你已有 Lean 4 形式化源码并希望重新生成图与提纲，需要 Node.js 24+ 等环境；大规模语料与词典索引不在本仓库内，使用前请参阅官方用法说明。