write-paper — fact graph → publishable paper
You are the main agent. This skill turns a project's verified fact graph into
a publishable LaTeX paper in a configurable house style: a standalone
\documentclass{amsart} .tex with a real manual bibliography, compiled to a
clean PDF, ready for arXiv / an Overleaf (or other) LaTeX git repo. It is the
publication sibling of human-summary (a reader-facing progress report with no
bibliography).
The heavy LaTeX work is delegated to a local codex at extra-high (xhigh)
reasoning — the same codex machinery the workers and the verify service already
use. The writer,
auditor, verifier, and reviser roles are wrapped behind the write-paper MCP
service (tools paper_write / reference_audit / reference_verify / paper_revise):
you call them with structured args, the tool assembles each role's prompt
internally (so the style guide and fact-graph bytes never enter your context) and
drives the codex with each role isolated by construction. The reference chain is
auditor (offline, flags) → verifier (online, checks) → reviser (edits). You
orchestrate the stages, call these tools, gate on compilation, and surface the one
or two real decisions to the operator.
When to use
- A project's target theorem is established in the fact graph and the operator wants the paper.
- The operator asks to write, revise, audit references for, or push the paper for a project.
Do not use it for the progress report (human-summary) or the internal strategy
synthesis (elaboration).
Source of content: the fact graph (never your memory)
Build the mathematics from the project's verified facts
(<project>/fact_graph/facts/*.md) and the verbatim goal in
<project>/PROBLEM.md — exactly as human-summary does, but for publication:
- Each fact's
## statementis fully-quantified and self-contained → render into the paper's theorems/propositions (clean LaTeX, do not paraphrase loosely). Its## proofis the argument;## intuitionfeeds a proof sketch where useful. - Load-bearing facts first: high dependency depth (headline results) and high
in-degree (key lemmas).
predecessorsgive you the internalTheorem~\ref{}cross-reference structure with zero invention. - Citations come structured, from the source. Each fact's
external_refs(key / authors / title / arxiv / year / cited_for) records the published results its proof cited.driver/seed_ledger.pyaggregates them across the project into the startingREFERENCE_LEDGER.md. Do not re-mine citations from prose — that is the #1 failure mode (hallucinated references). - Preserve all mathematics. Invent nothing — no assumptions, lemmas,
citations, theorem labels, or definitions that are not in the fact graph. If a
step is unclear, flag
[GAP: ...], do not smooth it over.
Paper workspace: <project>/paper/ (default) — and MULTIPLE papers per project
Per-project, alongside fact_graph/ and global_memory/:
<project>/paper/ # the DEFAULT paper (legacy paths — unchanged)
PROJECT_BRIEF.md # per-paper framing (interview the operator — see below)
REFERENCE_LEDGER.md # seeded from external_refs, verified by the auditor
REVISION_LOG.md # append-only round history
main.tex / main.pdf # the paper
<project>/TARGET.md # the DEFAULT paper's finalized target (danus finalize)
Seed the workspace from templates/ (copy *.template → the real names) if it
does not exist yet.
One project can hold MULTIPLE papers (e.g. a main theorem paper + a companion,
or several theorems each written up separately). Every paper_* tool and
danus finalize takes an optional paper_id:
paper_idomitted /"main"→ the DEFAULT paper on the legacy paths above (<project>/paper/+<project>/TARGET.md). Existing single-paper projects are byte-for-byte unchanged.- any other
paper_id(e.g.thmB) → an isolated workspace<project>/papers/<paper_id>/with its ownPROJECT_BRIEF.md/REFERENCE_LEDGER.md/REVISION_LOG.md/main.tex/TARGET.md. So N papers never collide — each has its own files.
There is one fact graph per project (<project>/fact_graph/); papers never
fork or re-filter it. A paper's facts are simply the transitive-predecessor
closure of its own headline set — the SAME closure primitive the single-paper
pipeline already uses, merely rooted at that paper's recorded target. The three
shapes are one model — a list of {paper_id, headline_fact_ids}:
- 1 paper / 1 theorem — the default: one entry,
paper_id="main". - N papers / 1 theorem each — N entries, each a distinct
paper_idand a single-fact headline; written in separate workspaces (no overwrite). - N papers / one multi-theorem paper — an entry whose
headline_fact_idsis a LIST of several targets; its fact set is the union closure of that list.
paper_id must be a single safe path segment (same validation as a project name);
it cannot escape the project dir.
Style source
Two generic, self-contained layers under style/, neither naming an author or a
field:
style/STYLE_GUIDE.md— the compact baseline house style (binding for voice: macros, theorem/proof shape, citations, cross-references, sentence-level rules).style/PAPER_STRUCTURE.md— the per-section content plan (binding for structure: what each part of the paper contains, by length tier — abstract, introduction, preliminaries, body, proofs, acknowledgements, bibliography). Field-neutral; uses placeholders, not any specific area's conventions.
Both are plain Markdown the operator may edit to encode their own preferences.
Imitating your own past papers is strictly optional — an add-on for authors who already have published papers, not a dependency:
style/anchors/— optional exemplar papers the operator drops in (one folder per paper, with its.tex) for theSTYLE_DISTILLERto learn from (feeding the unifiedSTYLE_GUIDE.md, which is the writer's single source of voice) and, optionally, for ONE of them — named deterministically by the brief'sstructural_exemplarfield — to be imitated for structure. Empty by default. The skill produces a complete, compilable paper from the two generic guides alone — anchors only make the output sound more like the operator's own writing. The writer never "picks the closest" anchor: voice is the distilled guide (all anchors), structure is the single brief-named exemplar (or none).
The role prompts under roles/ are generic and read directly; there is no
machine- or author-specific overlay.
Per-call run logs (diagnostics)
Every paper_* tool returns a log_path and writes a full on-disk diagnostic
record there — the complete assembled prompt, codex's full stdout and full
stderr (not just the tail), the honest result, the tool's post-processing
decisions, and the returned envelope. On a non-ok or surprising result, read
log_path for the full assembled prompt + codex stdout/stderr + tool decisions
before retrying or reporting — it lets you localize the failure (prompt vs codex
vs tool logic) instead of retrying blind. The small envelope (status / returncode
/ stderr_tail / flags / paths) is unchanged; log_path is additive. Run logs
live under the paper's own .runs/ (default <project>/paper/.runs/; a non-default
paper → <project>/papers/<paper_id>/.runs/), gitignored; set
DANUS_WRITE_PAPER_RUN_LOG=0 to opt out (then log_path is None).
Editorial quality bar — write WELL, not LONG (your judgment, applied at every stage)
You are the paper's editor. There is no hard length cap — some results genuinely
need many pages, and a fixed ceiling would only force you to mangle them. A good paper
is short because it is well-SHAPED, not because it was cut to a number. Shaping it is
YOUR job, and it starts before a single paper_write call:
- A paper is not a stack of facts — and YOU are the one who prevents that. The two
controls that decide the paper's shape are both yours: which facts you SELECT (the
support layer) and the editorial
instructionsyou write for eachpaper_write. So first UNDERSTAND the proof strategy as a whole; then select the load-bearing results that carry the argument and, in your instructions, direct that the support layer is developed in proper detail while every other fact contributes only the mathematical content the argument needs — stated, not re-narrated as a full proof. A hundred-fact closure rendered flat, one lemma after another, is exactly the failure this prevents: the writer renders what you hand it and how you tell it to, so the shape is set by your selection and instructions. Calibrate "how much detail" by the bar the whole-paper verifier uses (§5.5): a step a mathematics undergraduate could fill unaided may be abbreviated; anything they could not must be developed or cited. The mechanics of selecting and instructing are the BINDING RULE at stage 2; the levers you apply are below. - Length is a SYMPTOM, never a target. If a draft feels too long, the cause is
almost always a violation of the shaping principle above — re-proving something
citable, or re-narrating a routine computation — not "too many pages" as such. Fix
the cause, not the page count. A genuinely deep result that is long AFTER honest
citation and the right level of detail is SUPPOSED to be long; do not mangle it to
hit a number.
When one paper's worth of contribution truly spans a book, the human practice is a
SERIES of papers (the
paper_idsplit, lever #4) — an operator-initiated fork, not a cap you enforce on your own. - Density signals (health checks, not limits). A strong paper usually carries ~10–30 labeled results, one theorem-sized idea per section, and lemmas that exist because the narrative needs them. Red flags that the shaping broke down: 100+ labeled results; helper-lemma sprawl around a single proof; repeated setup/notation blocks; proofs that read as computation logs (transcription instead of exposition). These signal "go re-apply the shaping principle above", not "cut to N pages".
- The levers, in order — all serve the shaping principle above, none a page count. (1)
cite, don't re-prove (standard machinery → precise citations); (2) render at the
right granularity — full detail on the pivots, method+outcome on routine steps,
never one-lemma-per-fact; (3) curate which results the paper PRESENTS (a paper is
not every fact you proved; the support-layer BINDING RULE at stage 2); (4) SPLIT
into companion papers when the contribution genuinely spans more than one paper
(the
paper_idmechanism — a deep development becomes its own "Part II" / technical companion the main paper cites). - The reviser cannot globally compress — so get the granularity right the first time. Measured on a real paper: a dedicated compression-only round asked for −27K and delivered −0.5K; every "pay by compressing while adding" round under-paid while the paper inflated. A patch-style reviser executes located edits; it cannot execute global restructuring. So NEVER issue "compress the paper by N pages" — it silently under-delivers. What CAN work: YOU find specific mechanical redundancy yourself (a lemma proved twice, a definition declared twice, a duplicated setup block) and order its removal as POINT EDITS. The durable fix, though, is upstream: honest citation + right granularity when the section is first written.
The pipeline (you drive these stages in order)
0. PROJECT_BRIEF — interview the operator (do not invent)
If <project>/paper/PROJECT_BRIEF.md is absent, conduct a short interactive
interview with the operator to fill it: title, audience/venue, human authors
(and affiliations), which facts are the headline results, per-paper style
overrides, deadline. Write their answers into the brief. Never fabricate these —
they are the operator's call. (If the operator wants to skip and accept defaults,
record that; the writer then emits author placeholders.)
Pre-fill headline_fact_ids from the finalized target. When you seed the
brief, if the paper's TARGET.md exists (the default paper's <project>/TARGET.md,
or <project>/papers/<paper_id>/TARGET.md for a non-default paper — written by
danus finalize [--paper <paper_id>] when the operator approved the result as the
answer), copy its fact id(s) into the brief's headline_fact_ids field so the
finalized target is already the paper's headline. If TARGET.md is absent, leave
the field blank and ask the operator — and know that paper_write will
refuse with status="needs_target" until either the field is set or the
operator runs danus finalize <project> [--paper <paper_id>] <fact_id>. The skill
never guesses the target from the graph shape.
Two structured fields the brief carries (machine-read; keep the field: value
shape on its own line):
headline_fact_ids— the fact ids that ARE this paper's target results (the theorems it foregrounds). This is the backbone of the default: the writer is given the transitive-predecessor closure of these targets — NOT every proven fact — and the reference ledger is seeded from the same closure, so the writer's facts and the bibliography agree and the auditor never sees phantom rows for side lemmas the paper never cites. Pre-fill it from<project>/TARGET.mdif present, else ask the operator explicitly. If it is left blank AND noTARGET.mdis recorded, the target is UNSET andpaper_writerefuses (needs_target) rather than guessing — rundanus finalize <project> <fact_id>to record the target first.structural_exemplar— optional: the name of ONE folder understyle/anchors/whose STRUCTURE this paper should imitate. Voice always comes from the unifiedSTYLE_GUIDE.md; this names only the single structural exemplar. Blank = none. If the operator already has anchors, ask which (if any) to imitate structurally. Ifstyle/anchors/is empty, still offer once — "you can drop a few of your own papers intostyle/anchors/now to match your writing voice; want to? (a complete paper is produced either way)" — so the capability isn't hidden behind an empty folder. If they add some, run Stage 1a to distil them before writing.
1. Seed the reference ledger
python3 .../write-paper/driver/seed_ledger.py <project_dir> --headline <headline_fact_ids> --out <project>/paper/REFERENCE_LEDGER.md
# multiple papers: add --paper <paper_id> to scope the closure to that paper's
# recorded target and (with no --out) write the ledger into its own workspace:
python3 .../write-paper/driver/seed_ledger.py <project_dir> --paper <paper_id>
This aggregates the external_refs of the target-closure facts into
unverified rows. Pass the same headline_fact_ids you recorded in the brief
(stage 0) as --headline so the ledger's closure equals the writer's closure
(one closure, shared): the ledger then lists only references the paper's facts
actually cite — no phantom rows for proven-but-unused side lemmas. Omit
--headline to let the script resolve it identically (brief field → else the
finalized <project>/TARGET.md). If no target is recorded at all, the seed
refuses (matching the writer). (Verification is stage 4; --all-facts
restores the legacy all-facts seeding if ever needed.)
1a. Style preflight — distil the anchors if they changed (presence-triggered, once, operator-gated)
Before the writer stage, check whether the operator's own papers under
style/anchors/ need to be distilled into the unified STYLE_GUIDE.md. This is
the only automatic trigger for the STYLE_DISTILLER — without it, papers an
operator drops into anchors/ are silently ignored.
Trigger rule (all offline; the distiller only PROPOSES, never auto-applies):
- If
style/anchors/is empty → skip (the two generic guides produce a complete paper; nothing to distil). - If
anchors/is non-empty AND stale — its newest content is newer than thestyle/.distilled_atmarker, or the marker is absent — then run theSTYLE_DISTILLER(roles/STYLE_DISTILLER_PROMPT.md) to proposeSTYLE_GUIDE.mdupdates. Present the proposals to the operator; on accept, apply the accepted edits toSTYLE_GUIDE.mdand touchstyle/.distilled_at(record the distill time). On reject, still touch.distilled_atonly if the operator says the current guide stands (so a rejected-but-reviewed anchor set is not re-proposed every run) — otherwise leave the marker so it re-triggers. - If
anchors/is unchanged since the last distill (nothing newer than.distilled_at) → skip.
A tiny helper compares mtimes so the check stays clean:
bash .../write-paper/driver/anchors_stale.sh <skill_dir> # rc 0 = stale (distil), rc 1 = fresh/empty (skip)
Why operator-gated, never auto-applied: the distiller edits the guide that
governs every future paper; a bad distill would silently corrupt them all. The
distiller proposes; the operator accepts; only then does STYLE_GUIDE.md change.
This step is still optional in spirit — with no anchors it is a no-op — but when
anchors exist and changed, it runs so they are not ignored.
2. Write (PAPER_WRITER) — produce main.tex
Call the paper_write tool (the write-paper MCP service). You do not
build the prompt by hand and you do not read the style guide, the structure
plan, or the fact graph into your own context — the tool assembles all of that
internally and drives the codex, so the large bytes never enter your window.
First, curate — MANDATORY, and it is YOUR job, at EVERY level. paper_subgraph.
BINDING RULE — never hand a writer the whole closure. Every single
paper_writecall must be given a hand-picked support layer viafact_ids: the few key load-bearing results that call should PRESENT. It is forbidden to pass the full closure (or to omitfact_idsso the tool embeds it) unless the closure is single-digit (< 10 facts). Dumping all facts on one writer call is the root cause of overflow, the chunked fallback, and flat/bloated output — do not do it. If you think "this piece is small enough to just send its facts," check the count first; if it is ≥ 10, curate.This applies RECURSIVELY / fractally. A hard sub-result written as its own lemma-chapter is STILL a
paper_writecall, so it ALSO gets a curated support layer — not that sub-result's whole closure. If that chapter's support layer leans on a deeper load-bearing result, that deeper result becomes its OWN curatedpaper_writecall (its own chapter/sub-paper), which YOU then compose in (a written body slotted as a section — you do the stitching; see below). The paper is a TREE of curated single-pass writes you design and assemble, never one writer call swallowing a big fact set. "Pick the support layer" is the intelligence that stays with you at every node of that tree; the writer only renders what you hand it.
The target's full transitive closure can be hundreds of facts; embedding every proof would overflow a single writer pass. So do what a human author does: read a compact skeleton and SELECT the load-bearing subset to write up. Call
paper_subgraph(project=<project>, headline=[<target fact ids>|omit], paper_id=<paper_id|omit>)
It returns, deterministically (no codex, no writes), {status, headline, headline_source, count, facts} where each facts[i] is {id, statement (one-line), predecessors, dependents (in-closure in-degree — higher = more load-bearing), glossary_introduces} in topological order. Read it, pick the results the paper
should PRESENT (the headline theorems + the lemmas their proofs actually turn on —
NOT every granular intermediate step; those get cited), and write short editorial
instructions (how to section, what to foreground — and encode the editorial shaping
principle: support layer in detail, everything else stated minimally; see the
editorial bar). An unset target → the same
needs_target refusal as paper_write (run danus finalize first).
Then write — pass your selection + direction to paper_write:
paper_write(project=<project>, headline=[<target fact ids>], paper_id=<paper_id|omit for default>,
fact_ids=[<the load-bearing subset you selected>], instructions="<sectioning / emphasis>")
fact_ids— the subset frompaper_subgraphto PRESENT in full. The tool embeds only these (statement + proof) plus their direct-predecessor statements as\ref/\citecontext (the granular lemmas are cited, not reproduced) — so a curated paper fits ONE pass. Omitfact_idsONLY when the closure is single-digit (< 10 facts); on any larger closure omitting it (⇒ whole-closure embedding ⇒ chunked fallback ⇒ bloat) is the mistake the BINDING RULE above forbids. Unknown ids →status="bad_fact_ids"(no paper); ids outside the closure are kept with afact_id_warningsnote.instructions— your editorial direction, embedded verbatim as an authoritativeMAIN_AGENT_INSTRUCTIONSblock (wins over the writer's default structure, never over the PRIME DIRECTIVE / style voice / the mathematics).project— the project name (resolved underDANUS_AGENTS_ROOT).paper_id— WHICH paper in the project (multiple papers per project; one fact graph). Omit /"main"→ the default paper on the legacy<project>/paper/paths; any other id → the isolated<project>/papers/<paper_id>/workspace. The brief / ledger / TARGET.md the tool reads are rooted at that paper's workspace.headline— the paper's target fact ids (the headline results). This is the DEFAULT scoping: the tool embeds only the target's transitive-predecessor closure, in topological order, with zero invention — NOT every proven fact. Omitheadlineto let the tool resolve it the same way the ledger did: the brief'sheadline_fact_idsfield, else the finalized<project>/TARGET.md. The tool returnsheadline(the resolved target ids used) andheadline_source(arg/brief/target). If the target is UNSET (no arg, no brief field, noTARGET.md) the tool returnsstatus="needs_target"with acandidateslist (the terminal facts) and writes nomain.tex— rundanus finalize <project> <fact_id>(or fill the brief) and call it again. It never guesses.The structural exemplar is read from the brief's
structural_exemplarfield (one anchor to imitate for STRUCTURE); there is no per-call anchor arg. Voice always comes from the unifiedSTYLE_GUIDE.md.paper_writedoes NOT stop the worker swarm by default — entering write-paper does not always mean the whole problem is proven; a partial result can be written up while the swarm keeps exploring the rest. If you already stopped the swarm because the whole problem is proved (the completion rule inAGENTS.md/ the main-agent contract), this fork is moot — the swarm is already down; just write the paper. Otherwise (a partial result, exploration ongoing), you decide: at the start of write-paper (Stage 0) surface the fork to the operator — "Start the paper — stop the swarm's exploration, or keep it running? (A partial result can be written up while the swarm keeps proving the rest.)" On stop → callpaper_write(stop_workers=True)(ordanus stop <project>); on keep → the default (no stop). When you do request a stop it is graceful (never drops an in-flight verified round), idempotent, and failure-isolated; the tool reports it in aswarm_stopfield (result/noop/error/skipped).
Internally the tool embeds, in full: the role contract (roles/AGENTS.md — the
PRIME DIRECTIVE) and roles/PAPER_WRITER_PROMPT.md; the unified
style/STYLE_GUIDE.md (voice, distilled across all anchors) and
style/PAPER_STRUCTURE.md; boilerplate/acknowledgement.md; PROJECT_BRIEF.md
and the seeded REFERENCE_LEDGER.md; the fact-graph math of the target
closure (each fact's ## statement / ## proof / ## intuition + the
predecessor DAG, verbatim); and, iff the brief's structural_exemplar names an
existing anchor, that ONE anchor as a structural exemplar. Those codex-facing
fixed files (roles/, style/, boilerplate/) live under
agents/skills/write-paper/, not here — the MCP reads and embeds them; you never do. It
writes codex's stdout to <project>/paper/main.tex (a full \documentclass{amsart}
… \end{document}, real \ref/\cite, manual \begin{thebibliography}{99}).
The tool returns a small dict — {tex_path, status, returncode, headline, headline_source, selected_facts, fact_id_warnings, gaps, stderr_tail, log_path} (or
{status:"needs_target", message, candidates, log_path} when the target is unset,
or {status:"bad_fact_ids", unknown_fact_ids} when a selected id is not in the
graph). Honesty: it reports status="ok" only
on a zero exit with non-empty output; a nonzero codex exit, an empty artifact, or
a timeout is status != "ok" and nothing is written — do not treat a non-ok
result as a produced paper, and a needs_target result means you must record the
target first (danus finalize). headline/headline_source report which target
ids were used and where they came from. The gaps list is the [GAP: ...]
markers the writer left; act on them. The tool does not compile — the compile
gate is stage 3.
Auto-chunking — the extreme fallback. Curation (fact_ids) is the primary
answer to a large closure: a well-chosen subset writes in one pass. But if even the
prompt you assembled is still over budget (DANUS_PAPER_WRITE_CHUNK_CHARS, default
~800000 chars ≈ ~200K tokens) — a huge selection, or fact_ids omitted on a giant
closure — paper_write falls back automatically to chunked generation: a
planning pass (one codex call on the STATEMENTS ONLY of the set being written →
the fixed preamble + front matter + a section plan assigning every fact + the
bibliography), then per-section fill (one codex call per section, each given THIS
section's full proofs + the fixed preamble/labels + every other result's statement
for \ref), then a deterministic stitch into one main.tex. When you passed
fact_ids/instructions, the fallback chunks exactly that curated set and the
planner honors your instructions. Each call is still a NON-AGENTIC isolated codex
(empty cwd, everything embedded, no tool calls) — chunking is decided in Python and
sliced by section, not an agentic retrieval writer. The result carries chunked: true and sections: <n>. Under budget → the single-pass path runs unchanged.
Honesty is preserved: if the planner or any section writer returns non-ok, or a
deterministic coverage check finds an assigned fact unassigned/duplicated,
generation fails honestly (status="chunk_failed", failed_phase) and no
main.tex is written — a partial paper is never emitted. Cross-section coherence
(a \ref that does not resolve, a seam claim) is caught downstream by the compile
gate (stage 3) and paper_verify_math. If chunking keeps failing, prefer selecting
a smaller fact_ids subset, or split the work into multiple papers via paper_id.
Manual fallback — you assemble and drive codex yourself (last resort). If
paper_write returns status="chunk_failed" (or any non-ok you cannot resolve by
curating a smaller fact_ids subset or splitting into multiple papers), fall back to
the flexible manual path: you write the paper by driving codex directly. This is
the one place you assemble the codex prompt by hand — use your judgment (curate the
facts, restructure the sections, adjust emphasis) to get past whatever the
deterministic path choked on.
- Get the material. Read the failed run's
log_path— it holds the full assembled prompt (role contract + style guide + structure + brief + ledger + the fact bodies). Reuse it as-is, or re-assemble your own from the pieces you control: your curatedfact_ids(each fact's## statement/## prooffrom<project>/fact_graph/facts/*.md, or viapaper_subgraph),style/STYLE_GUIDE.mdstyle/PAPER_STRUCTURE.md, the brief, and the seededREFERENCE_LEDGER.md.
- Drive codex yourself. The prompt is large — write it to a temp file and put it
on stdin (never argv), and run the repo's codex wrapper at
xhigh, read-only (the same flags the tool uses — seedanus.authoring.driver):
In this fallback the bytes DO enter your context (you read/assemble the prompt) — that is the trade for flexibility, and it is acceptable because it is the rare last resort, not the hot path.bin/codex exec --model "$DANUS_MAIN_MODEL" --config model_reasoning_effort=xhigh \ --sandbox read-only --skip-git-repo-check - < /tmp/writer_prompt.md \ > <project>/paper/main.tex # or <project>/papers/<paper_id>/main.tex - Then re-enter the gates — verification is NOT bypassed. Your hand-written
main.texgoes through the SAME safety net as any tool-written one: the compile gate (stage 3), the reference audit/verify (stages 4/4.5), andpaper_verify_math(stage 5.5). The manual fallback loosens only how the paper is written, never how it is verified — a hand-written paper with a broken proof is still caught and still blocks deliver.
Honesty: exactly as on the tool path, a paper is "produced" only after it
compiles AND passes paper_verify_math. Never present a hand-written main.tex as
done before the gates pass.
2b. DEEP theorems — the CHAPTER TREE (write chapters with the writer; never dump facts on the reviser)
When the target's load-bearing content is too deep for one curated single-pass write
(hundreds of novel facts — e.g. a paper whose verifier gaps keep exposing deeper
sub-lemmas), do NOT try to close it by feeding fact piles to paper_revise — an
accretion of 100+ reviser-inserted lemmas produces a flat, disorganized blob and
converges terribly (measured). And do NOT fall back to the auto-chunker to "handle"
it. Instead, YOU author the paper as a tree of curated single-pass writes:
Design the tree (you, from the
paper_subgraphskeleton): a HOST frame + one chapter per deep development. The HOST's support layer is the main theorem, its direct combination inputs, and the chapter-level results — its instructions say: STATE each chapter-level result fully, with the one-sentence proof "The complete development is given in the dedicated technical section inserted below." (never a fabricated\ref), and prove ONLY the top-level assembly. Each CHAPTER is its ownpaper_writecall with its own workspace (paper_id=ch_*), its own brief/ledger (seed_ledger.py --paper), and a curated support layer (≤ ~10 facts — the BINDING RULE applies at every node); its instructions say: ONE short intro paragraph, a setup section, the lemmas in logical order, complete proofs; any prerequisite that is a result of the larger paper is declared explicitly in the setup ("we assume, established earlier in this paper: ...") — never re-proved, never hand-waved.Write the nodes — independent
paper_writecalls (parallelize freely); a chapter that overflows the writer's single-response limit is a sign to SPLIT it into sub-chapters (deeper tree), not to chunk. Compile each node; runpaper_verify_math(paper_id=ch_*)per chapter — its per-chapter verdict flags chapter-INTERNAL defects to fix now (a mangled induction, a dropped hypothesis) vs setup-imports (discharged at assembly, expected).Stitch (YOU are the editor — mechanical transforms only): extract each chapter's body (drop title/abstract/acks/bib), demote sectioning one level, prefix every
\label/\refwithchX:, wrap as\section{<title>}\label{sec:tech-chX}, insert the chapters in topological order before the host's assembly section, merge missing\usepackages /\newtheorems / macros /\bibitems into the host (dedupe by name/key), and replace each host pointer-proof sentence withSection~\ref{sec:tech-chX}. Keep the stitch as a rerunnable script; but every post-stitch edit lives on the merged file — re-stitching discards it, so freeze the tree first, stitch once, then edit.Stitch pitfalls (measured in a cold-start test — read before stitching):
- Record a manifest at design time. The pointer-proof sentences are
byte-identical and carry no chapter hint; some chapters are pure support (no
pointer at all). When you design the tree, record
{host theorem label → chapter paper_id}and the intended insertion order in the tree-design file — don't force the assembler to re-derive it by reading statements. - Ordering with delivered cycles. Chapters written independently may have GENUINELY cyclic setup-imports (A assumes B's result, B assumes A's). No insertion order fixes that at stitch time — pick the order that points the most load-bearing arrows backward, and leave the residual forward edges to the seam-discharge stage (conditional restatement + later discharge).
- "Assembly section" means the main-theorem proof section. If the host has OTHER full-proof sections that consume chapter results, they must ALSO end up AFTER the technical sections (relocate them), or the sequential verifier will reject the forward dependence.
- Macros: dedupe by name is unsafe on semantic conflicts. Same-name macros
with different bodies (e.g.
\joinas\operatorname{join}vs\vee) silently change a chapter's math if first-wins. Diff the bodies; on a semantic mismatch, rename in the chapter body. Preserve\renewcommandlines as-is (a chapter may legitimately renew a kernel command like\H); never downgrade them to\newcommand. - Packages must merge BEFORE
hyperref(load-order trap);\newtheoremdisplay-name variants for the same env — pick one. - Bibliography: import only
\bibitems whose keys are actually\cited; first-wins on duplicate keys; DROP/replace keys the verified ledger marks rejected/unverified (a mechanical stitch happily keeps bad keys — check the ledger). - The compile gate does NOT catch multiply-defined labels — after
namespacing, grep for duplicate
\label{...}yourself. - Chapter residue: each chapter body still carries its own disclosure
remark /
\noteannotations; the merged paper has N copies. Strip the duplicates at stitch time or queue them for the reviser — decide, don't ignore.
- Record a manifest at design time. The pointer-proof sentences are
byte-identical and carry no chapter hint; some chapters are pure support (no
pointer at all). When you design the tree, record
Discharge the seams (reviser rounds on the merged paper,
notes=trigger): rewrite every chapter setup item "established earlier in the larger paper" to a preciseTheorem~\ref{...}of THIS document; replace stale[cite/blocker]notes with precise\citeof ledger-verified keys; point the host assembly's invocations at the chapter theorems. SEAM ACYCLICITY (load-bearing): the whole-paper verifier reads SEQUENTIALLY — a proof may rely only on EARLIER results. Insert chapters in dependency order, and a setup item must point BACKWARD; if a chapter genuinely needs a LATER result, restate the affected theorem as explicitly conditional ("Assume (H). Then ...") and add, at the later point where (H) is proved, the one-sentence unconditional combination. Better: prevent it upstream — write chapter briefs so each chapter assumes only EARLIER chapters' outputs.Gates as usual on the merged paper: compile + reference chain (reuse the project's VERIFIED ledger for the merged workspace) +
paper_verify_math→ iterate the discharge (and, for a genuinely missing development, grow the tree: one more small curated chapter, stitched in — never a fact pile to the reviser).
3. Compile-verify (hard gate)
bash .../write-paper/driver/compile_verify.sh <project>/paper/main.tex
Runs the LaTeX engine (default pdflatex; xelatex/lualatex/tectonic via
TEX_ENGINE); fails on any LaTeX error or any undefined citation/reference. With
no TeX Live installed, TEX_ENGINE=tectonic (after bash scripts/install-tex.sh)
is the zero-dependency engine.
Do not proceed past a failed compile — feed the offending log lines back to a
codex revise round (stage 5) and recompile. The compile is the tool's /
orchestrator's gate, never the reviser's own self-check (the reviser runs in an
empty cwd and cannot compile). Authority boundary: paper_write does NOT
compile — run this gate once on the writer's first main.tex. paper_revise
retries the compile internally (re-drives the reviser with the failing log
until the .tex compiles, or fails honestly), so a paper_revise returning
compile="ok" has ALREADY compiled — do not redundantly re-run this gate after
it; only run it after paper_write or a hand edit. A broken .tex must never be
delivered or pushed.
4. Reference audit (REFERENCE_AUDITOR) — FLAG, never fabricate
Call the reference_audit tool.
reference_audit(project=<project>, paper_id=<paper_id|omit for default>)
The tool assembles the auditor prompt (roles/AGENTS.md +
roles/REFERENCE_AUDITOR_PROMPT.md + main.tex + REFERENCE_LEDGER.md — and
nothing else: the auditor never sees the fact graph, the style guide, or the
structure plan) and drives a codex that has no tools and no network. The
auditor only flags entries it cannot vouch for; verification is
reference_verify's job (Stage 4.5), not the auditor's. It returns
{findings, ledger_path, status, returncode, log_path}
and
writes no main.tex.
Take the auditor's findings and hand them straight to reference_verify (Stage
4.5) — that is where the flagged entries get checked online. As with
paper_write, a non-ok status means the audit run failed — do not treat empty
findings as a clean bibliography.
4.5 Reference verify (REFERENCE_VERIFIER) — online per-entry verification
Call the reference_verify tool with the auditor's findings.
reference_verify(project=<project>, findings=<the auditor's findings text>, paper_id=<paper_id|omit for default>)
This is the online half of the reference chain — auditor (offline, flags) → verifier (online, checks) → reviser (edits), symmetric to the proving chain
worker → verifier → fact_graph. The tool assembles the verifier prompt
(roles/AGENTS.md + roles/REFERENCE_VERIFIER_PROMPT.md + main.tex +
REFERENCE_LEDGER.md + the auditor's findings — and no fact graph, style, or
structure) and drives a codex over the networked path:
--dangerously-bypass-approvals-and-sandbox + the danus gateway at
DANUS_ROLE=verifier (exposing only search_arxiv_theorems, minimum privilege) +
codex's built-in web_search. The codex still runs in an empty cwd, so it cannot
touch the project tree; its only outward reach is the gateway's read-only tool +
web.
Per flagged entry it does: search_arxiv_theorems(statement/title) → best
arxiv_id → open https://arxiv.org/abs/<id> for the authoritative
authors/title/year + journal-ref, confirming it is the same paper (not merely
"a similar theorem exists"); non-arXiv references (textbooks / old journals) →
targeted web search at an authoritative source (publisher / DOI / zbMATH / DBLP).
It emits one verdict object per entry (verified / corrected / rejected /
unverifiable / retarget-internal) plus a one-line
…(truncated)