# Math Workspace
面向长篇数学写作与形式化协作的本地工作区：以 Markdown 保存正文，用稳定锚点、命题依赖、符号审计、Lean 对齐和本地 Reader 维持可检查的项目结构。
## 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
- Status: active
- Tags: math-writing, formalization, lean, codex, markdown, cli
## Content
Math Workspace 是一个面向长篇数学写作与形式化协作的本地工作区。正文仍然是人和 AI 都能直接阅读的 Markdown；稳定编号、引用、命题依赖、符号、Lean 锚点、审阅和发布则围绕同一份项目源码形成可检查的结构。
它不替人证明数学结论，也不会在后台悄悄改写书稿。能用确定性程序检查的事情交给扫描和校验；模型辅助能力必须由用户显式启动，其输出只作为审阅意见，而不是新的事实来源。
已有数学项目可以从 CLI、Reader、Codex plugin、项目特化 skill 或 Lean 中按需接入，不必一次启用全部能力。较稳妥的起点是先让项目索引和 Reader 正常工作，再逐步增加其他层。
## 项目入口
## 源码中保留身份
**稳定锚点，不手写编号**
章节、命题、公式、图和表使用稳定 hash；读者编号由当前结构生成，引用可承受章节插入、删除和重排。
**临时写作可以收束**
作者或 AI 可先使用 tmp-* 占位；finish 将其固化为正式身份，verify 检查断裂引用与遗留临时 ID。
**定义、符号与命题分开**
定义和符号是独立的查询系统，不会因为进入索引而被强行纳入命题编号或依赖图。
**所有结论回到原文**
Reader 和审阅结果都指向具体文件、行号或 h-* 锚点，不另造一份脱离源码的知识库。
```markdown
# #tmp-1 基础拓扑
## #tmp-2 紧性
定理 #tmp-3（有限子覆盖判据）：设 \(X\) 为紧空间。
由 @tmp-3 可知，每个开覆盖都有有限子覆盖。
```
编辑完成后运行：
```bash
math-workspace finish path/to/chapter.md
```
`finish` 固化临时身份，`verify` 则检查引用、迁移遗留和项目结构。稳定 ID 只解决身份与引用；正文读者看到的章节和定理编号，仍由当前书稿结构决定。
## Reader 与项目结构
本地 Reader 是当前主要界面。它读取项目源码，但不直接写入书稿；存在 `.math-workspace/config.json` 的项目才会启用增强的导航、引用回溯和审阅功能。
它提供多卷目录、定义查询、当前页符号、引用回溯、严格依赖标记、章节关系图和端点审阅。探索稿可以作为可折叠的集合继续阅读，而不提前进入 hash、依赖、Lean 或符号审计；正式书稿则可记录初稿、修订中、稳定稿等阶段与可选版本节点。对大型数学项目而言，难点往往不在于再打开一份 Markdown，而在于看清一个命题依赖什么、会影响什么，以及哪一段结构还没有被稳定地接管。
## 符号审计与 Lean 对齐
**符号审计是显式的审阅**
用户选定范围、Codex 模型与推理强度后，系统才提取符号绑定、生成同形候选并做语义复核。
```text
symbol bindings -> same-shape candidates -> semantic review
-> same / specialization / compatible reuse / conflict / uncertain
```
只有高置信、涉及专用符号且被复核为冲突的项目进入硬冲突列表；其余仍留给人工判断。审计不会自动改名，也不会成为 verify 的门禁。
**Lean 留下可解释的对齐证据**
扫描声明 docstring 中的正文锚点，记录覆盖候选、审阅过的契约基线、Lake 构建结果与依赖对照。
```text
manuscript anchor <-> Lean declaration
-> build evidence + dependency comparison
```
这些证据说明锚点存在、构建曾通过或依赖被观察到；它们不宣称原文与形式化实现已经语义等价，也不把覆盖率误称为证明完成度。
## 与 Codex 协作
标记工具支持普通选区、圈选、整条命题与擦除。每个标记只保存项目内的 Markdown 位置、可用的 formal 或公式锚点，以及来源 hash；它不复制书稿，也不创建另一套聊天历史。
在原生 Codex 任务中，MCP 可以返回这些定位，由 Codex 直接读取相关源码。它提供讨论标记、按稳定 ID 查询 formal 对象、有限深度的命题依赖切片、Lean 对齐证据、定义与符号等项目知识查询、已运行符号审计的读取，以及只读校验；真实讨论仍不被复制进另一套聊天历史：
```bash
math-workspace mcp
```
真实讨论、修改与审批留在 Codex 的任务历史中；Math Workspace 提供的是可回到源码的项目结构和精确位置，不把 Reader 变成另一个对话系统。
## 使用与发布
```bash
npm install -D math-workspace
npx math-workspace prepare
npx math-workspace serve .
```
`prepare` 创建或补全 `.math-workspace/config.json` 并生成可检查的索引；`serve` 启动只监听本机的 Reader。导出命令可生成普通 Markdown，或调用本机 Pandoc 与 LaTeX 工具链生成 PDF；稳定锚点不会泄漏到读者面对的编号中。
首次接入可按 `prepare → verify → serve` 进行：先确认扫描边界和 Reader，再按项目需要接入 Codex plugin、数学写作规则或 Lean。仓库附带可审阅的 `math-writing`、`editor`、`integrator` 与 `lean-formalization` 规则，先读目标项目自身约束，再只挑当前任务真正需要的一项。
早期的 VS Code 预览扩展已冻结在 `legacy/vscode-extension/`，不再参与当前构建、测试、打包或发布。现在的产品核心是本地 Reader、项目结构、形式化对齐和审阅能力，而不只是编辑器中的 Markdown 预览。
Math Workspace 适合篇幅长、结构会持续演化、内部引用密集的数学书稿、技术讲义、研究笔记和多卷手册。短文不必承担这套结构；只有编号、引用、符号、依赖和形式化边界开始彼此牵制时，它才会带来实际收益。