# Math Workspace A local workspace for long mathematical manuscripts, combining Markdown, a Reader, optional Lean review, and PDF editions built from selected chapters. ## 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-10-18 - Status: active - Tags: math-writing, markdown, lean, codex, publishing, cli ## Content Math Workspace brings writing, reading, review, and publication into a local workspace for long mathematical manuscripts. Keep the source in Markdown, use the Reader to look up definitions and symbols or compare Lean declarations, then compile selected chapters into a PDF edition. Chapters, prefaces, afterwords, and continuing-work pages share the same manuscript source throughout. Use it as a Codex plugin or through the standalone CLI. Lean is optional: ordinary writing, reading, and stable references work without a Lean project. Math Workspace is a development preview and is intended for use in a version-controlled project. ![Connections between mathematical prose, Lean declarations, and human review](/images/projects/math-workspace-banner.webp) ## Reading, references, and interactive figures The Reader offers navigation across books, volumes, and chapters, a page outline, definition and symbol lookup, and links back to referenced passages. It runs locally on `127.0.0.1`. Choose a Chinese or English interface and light or dark appearance, or follow Codex or the browser; these choices leave the manuscript and PDF languages unchanged. - **Stable references**: chapters, sections, propositions, equations, figures, and tables can carry stable `h-*` identifiers. References stay attached to their objects when files move, while displayed numbers follow the current structure. `finish` finalizes temporary identifiers; `verify` checks broken references and other structural issues. - **Math layout and exercises**: long formulas wrap at safe boundaries in narrow windows while retaining their original LaTeX, numbers, and source locations. Exercises have independent numbering within each chapter. Hints and solutions are collapsed by default, cross-file solutions link back to their questions, and exports retain the full content. - **Interactive and static figures**: self-contained HTML figures appear in place in the Reader, with a companion static image as a fallback. Markdown and PDF exports use the static images. Proposition graphs use dependencies explicitly declared in the manuscript. Users start symbol audits to check scope and meaning; the results remain advisory. Structural checks and symbol suggestions leave mathematical review to the author and reviewers. ![Book and volume navigation, mathematical prose, and Lean anchors in the Reader](/images/projects/math-workspace-reader-overview.webp) A public demo manuscript showing volume navigation, mathematical layout, and source anchors. ## Continue writing with Codex Select prose or a formula in the Reader to add the original Markdown or LaTeX, file location, and line range to the current Codex input. Add a question, then send it. Read-only MCP queries expose manuscript anchors, propositions, dependencies, terminology, and existing review evidence so the conversation can return to a specific passage. The sidebar **＋** starts a chapter, front matter, back matter, or continuing-work page. Review the destination book or volume and file path before adding the request to Codex. Once sent, the AI uses the CLI to create the file, write its contents, and validate the result. The Reader does not rewrite Markdown directly, and page creation refuses to overwrite existing files. An ordinary browser can copy the same request. ## Review prose alongside Lean Read a mathematical statement, its associated proof, and the corresponding Lean declarations side by side. Work through a page or chapter review queue, or open a complete Lean file with syntax highlighting, search, folding, line numbers, and source differences. **Refresh evidence** builds offline with the existing local toolchain and dependencies, recording declaration types, direct dependencies, and axiom dependencies, including `sorryAx`. Human verdicts, subclaim mappings, and unresolved issues are stored separately. Changes to the underlying material mark earlier decisions for review. A successful build does not establish semantic alignment between prose and formalization. On macOS, an explicitly started, read-only Lean session can query types, definitions, and proof goals without network access; the local toolchain and dependencies must already be available. AI review candidates enter an undecided draft, while a reviewer explicitly saves human conclusions. ![Compare a prose statement and proof with complete Lean source](/images/projects/math-workspace-lean-review.webp) Review statements, proofs, and Lean source together, with a separate record of human decisions. ## Manuscript history and signed versions Open **Versions & publication → Version history** to inspect historical manuscripts, file differences, and signature verification. Academic archives live in the project's `.math-archive/`, preserving original files and version relationships separately from rebuildable reading indexes and document-stage labels. Sign manuscript versions with Cosign / Sigstore and retain relationships between volume and whole-work versions. Signing requires an explicit action and identity authentication. Signature verification, source completeness, content changes, and Lean proof status are displayed separately. ## Publish selected chapters and keep extending the work In **Versions & publication → PDF publication**, choose this edition's volumes and chapters and combine its cover, front matter, contents, body, back matter, and continuing-work page. Chapters retain their numbers from the full manuscript, and references outside the edition are listed for review. Preview and download the PDF, edition manifest, and citation data after building. PDF generation requires local Pandoc and LaTeX tools. Enter work and edition DOIs manually, or use Zenodo to reserve a DOI, upload an edition, and publish it while retaining earlier editions. Zenodo requires a token in the local server process environment. Reservation, upload, and public release are separate actions; building a PDF does not publish it remotely. ![Review selected chapters, omitted chapters, and references outside a PDF edition](/images/projects/math-workspace-publication.webp) Review the edition's scope before building. All interface screenshots use a dedicated public demo manuscript. ## Installation and first steps The Codex plugin includes its CLI and Reader runtime: ```bash codex plugin marketplace add glenzli/marketplace --ref main codex plugin add math-workspace@glenzli-marketplace ``` After installation or an update, start a new Codex task and ask it to open Math Workspace for the writing project. Initialize an unconfigured project first. Alternatively, pin the standalone npm package as a project dependency: ```bash npm install -D math-workspace npx math-workspace init npx math-workspace open ``` After editing, run `npx math-workspace finish path/to/chapter.md` to finalize temporary identifiers and validate the selected scope. `verify` checks project-wide structure, while `doctor` inspects project discovery, Reader artifacts, and optional tools. npm and marketplace releases have separate schedules; available features depend on the installed version. See the [Usage Guide](https://github.com/glenzli/math-workspace/blob/main/docs/usage.md) for manuscript syntax, Lean review, and publication setup, and the [Installation Guide](https://github.com/glenzli/math-workspace/blob/main/docs/install.md) for adapting a project.