# Math Workspace
用于长篇数学写作的本地工具集：以 Markdown 保存正文，并处理稳定标识、引用、命题依赖、符号检查、Lean 对齐与发布导出。
## Metadata
- HTML: https://glenzli.com/projects/math-workspace/
- Markdown: https://glenzli.com/projects/math-workspace.md
- Collection: Projects
- Language: zh-CN
- Published: 2026-07-03
- Updated: 2026-08-29
- Status: active
- Tags: math-writing, formalization, lean, codex, markdown, cli
## Content
Math Workspace 是一组用于长篇数学写作的本地工具。正文保存在 Markdown 中；CLI 和 Reader 负责稳定标识、引用、命题依赖、符号检查、Lean 对齐记录与发布导出。
当前版本仍处于开发预览阶段，命令、配置和生成数据格式可能变化。项目以源码为准，索引和报告可以检查、删除并重新生成。结构扫描只处理可机械判断的问题，数学结论仍由作者、审阅者和所使用的形式化工具确认。
## 项目入口
## 稳定标识与引用
**标识与编号分开**
章节、小节、命题类对象、公式、图和表可以使用稳定的 h-* 标识；读者看到的编号仍按当前结构生成。
**临时标识可以固化**
新增内容先使用 tmp-*；finish 将其替换为稳定标识，并执行一次校验。
**结构问题单独检查**
verify 检查断裂引用、残留临时标识和迁移问题，不把结构一致性当作数学正确性。
**定义与符号分别查询**
定义和符号使用各自的查询数据，不会因为进入索引而参与命题编号。
```markdown
# #tmp-1 基础拓扑
## #tmp-2 紧性
定理 #tmp-3（有限子覆盖判据）：设 \(X\) 为紧空间。
证明：...
由 @tmp-3 可知，每个开覆盖都有有限子覆盖。
```
```bash
math-workspace finish path/to/chapter.md
math-workspace verify
```
## Reader 与依赖审阅
本地 Reader 提供多卷导航、目录、定义查询、当前页符号、引用回溯、正文刷新和命题关系查看。它只监听 `127.0.0.1`，并且只为包含 `.math-workspace/config.json` 的项目启用工作区界面。
依赖审阅读取命题中显式声明的严格依赖，生成上下游关系、章节图和端点报告。普通说明文字不会自动成为依赖边。相关索引和报告都从项目源码生成，可以随时删除并重建。
## 符号检查与 Lean 对齐
**符号检查由用户启动**
Codex 检查同形符号及其作用域和含义，结果按内容缓存并作为审阅报告展示。
检查结果不会改写正文，也不进入 verify 门禁。
**Lean 对齐记录可核对的证据**
配置 Lean 项目后，可以扫描声明 docstring 中的正文锚点，记录 Lake 构建结果，并对照两边的直接依赖。
这些记录用于检查锚点、构建和依赖，不自动证明正文与形式化实现语义等价。
## Codex 上下文
Reader 标记保存文件位置、可用锚点和来源 hash。只读 MCP 工具可以查询标记、命题、有限深度的依赖关系、Lean 状态、项目术语、既有符号检查结果和校验结果，让讨论仍能回到具体源码。
```bash
math-workspace mcp
```
## 安装与导出
```bash
npm install -D math-workspace
npx math-workspace init
npx math-workspace open
```
`init` 创建或补全 `.math-workspace/config.json` 并生成项目索引；`open` 从当前目录查找项目根目录并启动本地 Reader。Codex plugin 也可以从公开 marketplace 安装，自带 CLI 与 Reader 运行时。
导出命令可以生成合并或分文件 Markdown，也可以调用本机 Pandoc 与 LaTeX 工具链生成 PDF。PDF 导出需要本机另行安装这些工具。
早期 VS Code 扩展已冻结在 `legacy/vscode-extension/`，不参与当前构建、发布和支持。