# Math Workspace

Local tools for long-form mathematical writing, with Markdown manuscripts, stable identifiers, references, proposition dependencies, symbol checks, Lean alignment, and publication exports.

## Metadata

- HTML: https://glenzli.com/en/projects/math-workspace/
- Markdown: https://glenzli.com/en/projects/math-workspace.md
- Collection: Projects
- Language: en
- Published: 2026-07-03
- Updated: 2026-08-29
- Status: active
- Tags: math-writing, formalization, lean, codex, markdown, cli

## Content

Math Workspace is a set of local tools for long-form mathematical writing. Manuscripts remain in Markdown, while the CLI and Reader handle stable identifiers, references, proposition dependencies, symbol checks, Lean alignment records, and publication exports.

The current release is a development preview. Commands, configuration, and generated-data formats may change. Project source remains authoritative, and generated indexes and reports can be inspected, removed, and rebuilt. Structural scans cover mechanically decidable problems; mathematical claims remain the responsibility of authors, reviewers, and the formal tools they use.

## Project Entry

  ![Math Workspace for mathematical writing, dependencies, symbols, and Lean alignment](/images/projects/math-workspace-banner.webp)

## Stable Identifiers And References

    **Identity is separate from numbering**
    Chapters, sections, proposition-like objects, equations, figures, and tables can use stable <code>h-*</code> identifiers while reader-facing numbers continue to follow the current structure.

    **Temporary identifiers can be finalized**
    New structure begins with <code>tmp-*</code>. <code>finish</code> replaces those placeholders with stable identifiers and runs validation.

    **Structural checks stay narrow**
    <code>verify</code> finds broken references, remaining temporary identifiers, and migration problems without treating structural consistency as mathematical correctness.

    **Definitions and symbols remain separate**
    Definitions and symbols use their own lookup data rather than entering proposition numbering simply because they are indexed.

```markdown
# #tmp-1 Basic Topology

## #tmp-2 Compactness

Theorem #tmp-3 (Finite Subcover Criterion): Let \(X\) be compact.

Proof: ...

By @tmp-3, every open cover has a finite subcover.
```

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

## Reader And Dependency Review

The local Reader provides multi-volume navigation, contents, definition lookup, current-page symbols, reference recall, source refresh, and proposition relationships. It binds only to `127.0.0.1` and enables the workspace interface only for projects containing `.math-workspace/config.json`.

  ![Math Workspace proposition dependency review](/images/projects/math-workspace-dependency-review.webp)

Dependency review reads strict dependencies declared explicitly on propositions, then produces upstream and downstream relationships, chapter graphs, and endpoint reports. Ordinary explanatory prose does not create dependency edges. The supporting indexes and reports are generated from project source and can be removed and rebuilt.

## Symbol Checks And Lean Alignment

      **Symbol checks are user-initiated**
      Codex checks same-shape symbols, their scopes, and their meanings. Results are cached by content and presented as a review report.

The report neither rewrites the manuscript nor becomes part of the <code>verify</code> gate.

      **Lean alignment records inspectable evidence**
      Once a Lean project is configured, Math Workspace can scan manuscript anchors in declaration docstrings, record Lake build results, and compare direct dependencies on both sides.

These records cover anchors, builds, and dependencies; they do not establish semantic equivalence between a manuscript and its formalization.

  ![Math Workspace symbol check report](/images/projects/math-workspace-symbol-audit.webp)

## Codex Context

Reader marks retain file locations, available anchors, and source hashes. Read-only MCP tools can query marks, propositions, bounded dependency slices, Lean status, project terminology, existing symbol checks, and validation results, keeping discussion tied to concrete source.

```bash
math-workspace mcp
```

## Installation And Export

```bash
npm install -D math-workspace
npx math-workspace init
npx math-workspace open
```

`init` creates or completes `.math-workspace/config.json` and generates the project index. `open` finds the project root from the current directory and starts the local Reader. The Codex plugin can also be installed from the public marketplace and carries its own CLI and Reader runtime.

Export commands produce combined or split Markdown and can call local Pandoc and LaTeX tools to generate PDF. Those tools must be installed separately for PDF export.

The early VS Code extension is frozen under `legacy/vscode-extension/` and is excluded from current builds, releases, and support.