(working name — rename freely)
A framework for turning an AI-written math paper plus a Lean formalization into two synchronized, verifiable outputs:
- LaTeX/PDF for arXiv (generated from a PreTeXt source of truth);
- Structured HTML with reader-controlled detail levels, notation hovers, and per-statement links into the formalization — optionally wrapped in a whole project site with API docs, Verso blueprints, and a public development record.
What is canonical: the editable inputs are the LaTeX draft plus the
committed sidecars (insertions, author metadata, notation decisions,
directives, configuration). paperforge deterministically assembles these
into a canonical PreTeXt intermediate representation — source/ is
generated, never hand-edited — from which both outputs build. To change
existing prose, edit the draft (the paper-view editor splices it for you);
to add persistent paperforge-only material, use content/insertions/.
Math stays LaTeX inside <m>, so the XML authoring cost falls on the
tooling, not the author. See docs/ARCHITECTURE.md
for the requirement-by-requirement design.
The exercised instance is the G_Q2 paper: https://roed314.github.io/gq2/ — paper, PDF, two independent formalizations with per-statement badges, blueprints, API docs, and the full AI-development record with token accounting.
- A faithful converter (
ingest/tex2ptx.py): deterministic LaTeX→PreTeXt with a numbering simulator (validated against pdflatex's.aux), stablexml:ididentity across renumberings, author metadata, alphabetic bibliography labels, and a byte-span source map that powers in-browser editing of the original draft. - The reading experience: knowl proofs, a global detail slider with per-proof tiers, notation hovers with definition-site highlighting, section-summary popups, equation-range knowls, dark mode, print/HTML content splits.
- Formalization linkage:
<lean>badges per statement (multiple independent formalizations, color-coded), inline doc knowls, doc-gen4 subsets, Verso blueprints with Lean-derived dependency graphs, and an axiom census whose citations are validated like everything else. - Eight deterministic validators (
paperforge-check): Lean refs resolve, summaries present, directives fresh, notation defined-before-use, numbering drift, reference/citation coverage, plagiarism n-grams, artifact drift. - The author cockpit: a local review dashboard + the paper view as editor — margin marks, decision cards, statement/proof/paragraph editing that splices the LaTeX draft and rebuilds, all autosaved into committed JSON artifacts.
- Provenance throughout: every generated item stamped with its generator, every applied change a discrete commit, and optional development-record pipelines (token ledger, sanitized session corpora, cost dashboard) for publishing how the paper was made.
- This repo (the tool): converter + generators (
ingest/), validators (validators/), site assembly (sitegen/), development-record pipelines (records/), the review server (review/), agent-executed skills (skills/), instance scaffolding (pretext-template/,templates/), and docs. No paper content lives here. - An instance repo (one per paper): the PreTeXt source,
paper.toml, the style corpus, reference PDFs, decision artifacts, and pointers to the Lean project(s). Scaffolded by thepaper-initskill.
Lessons flow one way: instance-specific tooling gets generalized back into the tool, parameterized by config, and the instance copy is deleted.
Every requirement is handled by exactly one of:
- Validators (
validators/, Python) — deterministic, objective, CI-gating. They never write; a failure means a human or a skill must fix something. - Skills (
skills/, agent-executed instruction files) — generative, subjective, re-runnable. Draft ingestion, bridging text, summaries, novelty exposition, background sections, grammar. Each ends with a Contract block (reads/writes/gate/provenance) so any agent that honors it is a valid executor — acceptance is enforced by the validators and author review, never by trusting the generator.
If a check can be made objective, it is a validator. Everything else is a skill.
# Tool setup (once)
git clone https://github.com/roed-math/paperforge
python3 -m pip install -e paperforge -e paperforge/validators
paperforge selftest # runs the bundled fixture end to end
# Instance setup
mkdir my-paper && cd my-paper && git init
paperforge init . --title "My Paper" --slug my-paper \
--lean-root ../my-paper-lean # or --no-lean
# Put the LaTeX draft at inputs/draft/main.tex, then:
paperforge doctor # environment + state, one next command
paperforge ingest --bootstrap # numbering + CANDIDATE declaration map
# review crosswalk/lean-decl-map.candidate.json, then:
paperforge accept lean-decl-map
paperforge build web
paperforge check # the eight validators
paperforge review # the author cockpitpaperforge selftest answers "is my environment right?" separately from
"is my paper right?" — it runs the sequence above against the public
fixture (examples/minimal-paper) in a throwaway
directory. CI runs the same path on Ubuntu and macOS, including from a
directory with spaces in its name. The generative passes (summaries,
bridging, novelty, grammar) remain agent-executed skills on top of this
deterministic core; docs/GETTING-STARTED.md
is the milestone-by-milestone walkthrough.
| dir | what |
|---|---|
paperforge/ |
the paperforge command: init, selftest, doctor, status, ingest/accept, build, check, review, migrate |
ingest/ |
LaTeX→PreTeXt converter; crosswalk, notation, axiom-census, trust-table, novelty, corpus tools |
validators/ |
the paperforge_validators package (pip-installable; paperforge-check = paperforge check) |
sitegen/ |
project-site assembly: version footers + drift gate, homepage knowls, favicon, preview watcher |
records/ |
optional development-record pipelines: token ledger, sanitized corpora, dashboard apply/check |
review/ |
the review server + the paper-view editor/margin/marks layers it injects |
skills/ |
agent-executed passes, one SKILL.md each, Contract blocks throughout |
pretext-template/ |
instance scaffold: XSL conversions, publication files, web-assets UI layer, authors sidecar |
templates/ |
instance scaffold: the annotated paper.toml, agents/style-corpus/reference guidance, the deploy + vendor scripts |
docs/ |
see the index below |
| doc | covers |
|---|---|
| GETTING-STARTED | empty directory to built, validated paper: install, selftest, scaffold, the loop |
| CONFIGURATION | every config key: layers, path semantics, defaults, deprecations |
| TROUBLESHOOTING | first-build states, environment mismatches, drift gates, diagnostics |
| DEVELOPMENT | paired tool/instance development: editable install, provenance, parity discipline |
| ARCHITECTURE | the design: requirement→mechanism map, moving-target strategy, agent-swap interface |
| DIRECTIVES | the human-in-the-loop control surface (inline markers + sidecar queue) |
| NOTATION | the notation map, hovers, disambiguation, order checking |
| REFERENCES | citation completeness, axiom coverage, locator pins, bib labels |
| PLAGIARISM | the n-gram guard and its provenance labeling |
| NOVELTY | the claims dossier: five novelty classes and their evidence |
| HTML-FEATURES | the interactive layer's feature contracts and gotchas |
| REVIEW | the review dashboard and in-chat review |
| EDITOR | the paper view as editor: lanes, source map, structural gates |
| DEPLOYMENT | site structure, build/deploy scripts, version footers, records pipelines |
| AI-POLICIES | publisher policies on AI-assisted mathematical writing |
Everything above is implemented and running on the first instance; the
validators, converter, sitegen and records pipelines — and now the
paperforge build web orchestration — were all verified byte-for-byte
against it when generalized, and the onboarding path runs in CI against
the public fixture. Known rough edges for a second project:
- One exercised real instance. The fixture and
paperforge selftestcatch onboarding defects, not real-paper complexity; the second paper will find assumptions. - One numbering profile. The simulator implements (and names)
amsart-shared-section-theorems-global-equationsand refuses others — verify against your draft's.auxbefore trusting a new convention. - Generative skills are not installed commands. They are instruction
files an agent follows (Claude Code today); there is no
paperforge run <skill>driver yet — deliberately deferred until a second harness is real. - PreTeXt 2.43–2.45 is what's exercised (2.43.2 on the first
instance, whatever
pip install pretextgives CI — 2.45.0 today); the XSL overrides ride on core internals (and two upstream-bug workarounds) that may shift — the postprocessing stages error rather than silently ship when the emitted patterns change. - The records pipelines' worked example lives in the first instance's
records-pipeline/, not here; the config shapes are documented in eachrecords/module's docstring.
paperforge produces AI-assisted mathematics, so its design answers to an active community conversation and a fast-moving policy landscape.
Publisher policies. docs/AI-POLICIES.md surveys how mathematics publishers (AMS, SIAM, Elsevier, Springer, Wiley, Taylor & Francis, Cambridge, arXiv, …) treat AI-assisted writing — what must be disclosed, in what form, and what is prohibited — and how paperforge's provenance record is designed to generate the required disclosures mechanically.
Discussions worth reading.
- Terence Tao, Machine-Assisted Proof, Notices of the AMS, January 2025 — the standard survey of how proof assistants, ML, and LLMs are entering research practice; see also his running machine-assisted proof posts.
- The Bulletin of the AMS double special issue Will machines change mathematics? (April and July 2024) — perspectives from Avigad (Mathematics and the formal turn), Venkatesh, Granville, Cheng, Harris, and the Buzzard–Commelin–Topaz and Shulman formalization essays.
- AMS white paper, Artificial Intelligence: Publishing in Mathematics — the society's own analysis of what AI assistance means for its journals.
- Steinberger et al., Using Generative AI for Literature Searches and Scholarly Writing, Notices of the AMS, January 2024 — the integrity risks (hallucinated citations above all) that several of paperforge's validators exist to counter.
- Michael Harris's Silicon Reckoner — a sustained critical counterpoint on the automation of mathematics.
- Empirics on the policy gap: Academic journals' AI policies fail to curb the surge in AI-assisted academic writing and Academ-AI, documenting undisclosed use — the failure mode paperforge's write-time provenance is built to make impossible.
GPL v3 or (at your option) any later version — see LICENSE.