项目

Math Workspace

发布于: 2026-07-03最后编辑: 2026-08-29active

math-writingformalizationleancodexmarkdowncli

Math Workspace 是一组用于长篇数学写作的本地工具。正文保存在 Markdown 中；CLI 和 Reader 负责稳定标识、引用、命题依赖、符号检查、Lean 对齐记录与发布导出。

当前版本仍处于开发预览阶段，命令、配置和生成数据格式可能变化。项目以源码为准，索引和报告可以检查、删除并重新生成。结构扫描只处理可机械判断的问题，数学结论仍由作者、审阅者和所使用的形式化工具确认。

项目入口

标识与编号分开章节、小节、命题类对象、公式、图和表可以使用稳定的 h-* 标识；读者看到的编号仍按当前结构生成。

临时标识可以固化新增内容先使用 tmp-*；finish 将其替换为稳定标识，并执行一次校验。

结构问题单独检查verify 检查断裂引用、残留临时标识和迁移问题，不把结构一致性当作数学正确性。

定义与符号分别查询定义和符号使用各自的查询数据，不会因为进入索引而参与命题编号。

# #tmp-1 基础拓扑

## #tmp-2 紧性

定理 #tmp-3（有限子覆盖判据）：设 \(X\) 为紧空间。

证明：...

由 @tmp-3 可知，每个开覆盖都有有限子覆盖。

math-workspace finish path/to/chapter.md
math-workspace verify

本地 Reader 提供多卷导航、目录、定义查询、当前页符号、引用回溯、正文刷新和命题关系查看。它只监听 127.0.0.1，并且只为包含 .math-workspace/config.json 的项目启用工作区界面。

依赖审阅读取命题中显式声明的严格依赖，生成上下游关系、章节图和端点报告。普通说明文字不会自动成为依赖边。相关索引和报告都从项目源码生成，可以随时删除并重建。

符号检查由用户启动Codex 检查同形符号及其作用域和含义，结果按内容缓存并作为审阅报告展示。

检查结果不会改写正文，也不进入 verify 门禁。

Lean 对齐记录可核对的证据配置 Lean 项目后，可以扫描声明 docstring 中的正文锚点，记录 Lake 构建结果，并对照两边的直接依赖。

这些记录用于检查锚点、构建和依赖，不自动证明正文与形式化实现语义等价。

Reader 标记保存文件位置、可用锚点和来源 hash。只读 MCP 工具可以查询标记、命题、有限深度的依赖关系、Lean 状态、项目术语、既有符号检查结果和校验结果，让讨论仍能回到具体源码。

math-workspace mcp

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/，不参与当前构建、发布和支持。