-
-
Emdash proof case study: a 192-page development book connects mathematical exposition to checked Lambdapi evidence.
-
Codex proposes a source diff while Arrowgram renders the same Markdown and typed diagram JSON as a paged paper.
-
Arrowgram's workflow: Codex edits typed source, humans refine diagrams visually, and GetPaidX publishes the result.
Inspiration
Research diagrams rarely live alone. They belong inside a proof, paper, lecture, or book, yet the usual workflow splits the work across a drawing tool, source files, a local development environment, and a publishing system.
That split is especially awkward for AI coding agents. Codex is strongest when it can inspect, edit, validate, and diff durable files. A human is strongest when they can see the diagram, move a node, and judge whether the mathematics communicates clearly.
We built Arrowgram so they can work on the same artifact.
We did not bolt a chat panel onto a canvas. We made the diagram and paper themselves legible to Codex, editable by people, runnable in a browser, and publishable from a hosted AI workspace.
What Arrowgram does
Arrowgram is a visual editor and typed authoring system for commutative diagrams, research papers, books, and slide decks.
Its source of truth is a small set of ordinary files:
arrowgram.workspace.jsondescribes the workspace;diagram.jsonstores a standalone diagram using a strict schema;paper.mdstores a paper, book section, or Reveal.js deck;paper.csscontrols publication styling.
Codex can edit those files directly. Arrowgram validates them and opens the same content in a visual editor. A person can then drag nodes, connect arrows, adjust properties, or review the rendered paper, and those changes persist back to the workspace files.
From the same source, Arrowgram can produce SVG, PNG, TikZ-CD, paged HTML/PDF-oriented documents, Reveal.js presentations, and static publication sites.
One project, two Codex plugins
Arrowgram has two complementary Codex integration paths.
The Arrowgram plugin: local and file-first
The open-source Arrowgram plugin teaches Codex to initialize, inspect, edit, validate, preview, diff, snapshot, and build a local Arrowgram workspace through @hotdocx/arrowgram-agent.
npx -y @hotdocx/arrowgram-agent init --type paper --root .
npx -y @hotdocx/arrowgram-agent validate --root .
npx -y @hotdocx/arrowgram-agent dev --root . --port 4173
npx -y @hotdocx/arrowgram-agent build --root . --out dist
This path is open source, local-first, and works with normal Git workflows.
The GetPaidX plugin: hosted and publishable
The GetPaidX Codex plugin connects the user's own Codex CLI or app to https://getpaidx.com/api/mcp through OAuth. It exposes curated tools for the complete Arrowgram cloud workflow:
- create or select a GetPaidX post;
- start an Azure-hosted
arrowgram_webworkspace; - read or write the allowlisted Arrowgram source files;
- inspect the source diff;
- build static
dist/index.htmloutput; - save a Git-backed workspace snapshot;
- publish a stable artifact site;
- close the workspace session.
The same workflow is also available in the GetPaidX browser UI. A user can open the workspace's visual editor, terminal, or in-container Codex session without installing the formal-math or publishing stack on their own machine.
The important boundary is that GetPaidX does not invent a second cloud-only document model. The hosted controller, external Codex plugin, in-container Codex, and browser editor all operate on the same Arrowgram files.
End-to-end workflow
A user can ask:
Create a GetPaidX post with an Arrowgram workspace, draft a paper about pullbacks, add a commutative diagram, show me the diff, save a snapshot, and publish it.
Codex can then use the GetPaidX MCP tools to provision the workspace and manage its lifecycle, while the Arrowgram skill supplies the authoring rules for the diagram and paper themselves.
The result is not only a response in a chat window. It is a persistent workspace with inspectable source, a visual editing surface, versioned snapshots, a reproducible build, and a shareable publication.
How we built it
Arrowgram is an npm-workspace monorepo with three main public packages:
@hotdocx/arrowgramowns the Zod schema, geometry engine, computed model, and React SVG renderer;@hotdocx/arrowgram-webowns the visual workspace, paper editor, preview, and browser persistence;@hotdocx/arrowgram-agentowns the file watcher, bridge API, validation, diff/snapshot behavior, and static builds.
The editor uses React, TypeScript, Vite, Zustand, IndexedDB, KaTeX, Mermaid, Vega-Lite, Paged.js, and Reveal.js. Core geometry and schema behavior is tested with Vitest; browser and bidirectional editing flows are tested with Playwright.
GetPaidX supplies post-backed persistent workspaces, Azure controller allocation, OAuth-protected MCP access, live preview, Git-backed snapshots, and artifact-site publishing. Its curated MCP tools enforce source-file allowlists and keep generated dist/ output separate from editable source.
Emdash: the proof that the workflow scales
Our case study is Emdash, an experimental Lambdapi specification for functorial type theory and a future proof assistant for directed higher-dimensional mathematics.
Its headline checked result constructs a directed walking endomorphism and establishes the carrier equivalence:
Hom_WalkingEnd(*,*) ≃ Nat
Emdash also produces the development book Functorial Type Theory: Univalent Foundations for Mathematics. The current 0.2.0-dev artifact is a 192-page tagged PDF assembled from 32 ordered Markdown sources. Its evidence registry maps 107 claims to implementation owners and reviewer evidence, distinguishing checked results, formal consequences, mathematical development, and research boundaries.
The Emdash renderer uses the published Arrowgram package inside a Markdown, KaTeX, Mermaid, Vega-Lite, Paged.js, and headless-Chromium pipeline. The release checks embedded diagram JSON, links, pagination, text extraction, fonts, accessibility, and deterministic PDF output.
This forced Arrowgram to handle the details that a small demo avoids: dense mathematical typography, long-document pagination, embedded diagrams, source provenance, formal-status labels, browser review, and reproducible publishing.
How we used Codex and GPT-5.6
We used Codex with GPT-5.6 as an engineering and research-authoring collaborator across Arrowgram, GetPaidX, and Emdash.
Codex helped us:
- design and implement the two-plugin boundary between local authoring and hosted workspace management;
- trace file/browser synchronization and canvas-persistence bugs across the renderer, editor, and bridge;
- build the OAuth/MCP workflow for creating, editing, diffing, building, snapshotting, and publishing cloud Arrowgram workspaces;
- keep source edits scoped to safe, allowlisted files instead of generated output;
- develop the Emdash book structure and connect prose claims to Lambdapi evidence;
- run focused unit, integration, browser, build, and publication checks;
- maintain workflow documentation alongside the code.
GPT-5.6 was most useful when the task crossed repository boundaries: understanding which layer owned a behavior, preserving the artifact contract, and validating the result rather than stopping at code generation.
Challenges we ran into
One source of truth across four editing surfaces
Local Codex, remote Codex over MCP, in-container Codex, and the browser editor must not create competing copies of a document. We kept the workspace files authoritative and built explicit file-change, diff, snapshot, and build operations around them.
Separating source from generated output
Agents must edit paper.md, paper.css, diagram.json, and the workspace manifest—not patch dist/index.html. Both plugins document and enforce that boundary.
Making cloud automation safe
The hosted plugin uses OAuth-scoped identity, curated lifecycle tools, catalog-gated API discovery, source-file allowlists, and approval-aware mutation routing. Arbitrary workspace paths and arbitrary API URLs are not exposed as a shortcut.
Preserving mathematical honesty
A polished research book can make exposition look formally verified. Emdash therefore records whether a claim is checked, a formal consequence, mathematical development, or an open research boundary.
Accomplishments that we're proud of
- Arrowgram works as both a human visual editor and a Codex-editable artifact format.
- The local CLI and hosted GetPaidX workflow share the same source model.
- The public GetPaidX plugin completed a production OAuth login and an end-to-end hosted Arrowgram workspace smoke through source edit, diff, build, and snapshot.
- Hosted workspaces can be reviewed visually, saved as Git-backed snapshots, and published as static artifact sites.
- Emdash exercises the stack on a substantial formal-mathematics and book-production project rather than a synthetic landing-page demo.
- The core packages and agent bridge are published on npm and the Codex plugins are distributed from the public Arrowgram repository.
What we learned
The best interface for an AI coding agent is often not another chat abstraction. It is a durable artifact model with clear ownership, strict validation, readable diffs, and reproducible build commands.
We also learned that human and AI editing are complementary. Codex is effective at structural changes, cross-file reasoning, repetitive authoring, and validation. The visual editor is better for spatial judgment and direct manipulation. GetPaidX adds the missing operational layer: a persistent environment where both can work, review, snapshot, and publish.
What's next
We plan to:
- add more public Arrowgram starter workspaces and mathematical templates;
- make the hosted Arrowgram onboarding path shorter and more discoverable;
- improve parity across editor, static build, Paged.js, Reveal.js, Mermaid, and Vega-Lite output;
- expand visual-regression and accessibility coverage;
- add richer workspace history and publication examples;
- continue using Emdash as a demanding integration test for research papers and books.
Log in or sign up for Devpost to join the conversation.