Specialized Claude Code agents for rigorous AI research workflows, designed to support high-impact publications at top-tier venues (NeurIPS, ICML, ICLR, JMLR, Nature Machine Intelligence).
This repository contains agent specifications organized into six categories:
- Research Workflow — A structured 10-phase methodology for taking research from problem framing through submission, plus cross-phase tools including session memory and literature synthesis.
- Research Shaping — A diverge-then-converge layer that turns a body of work into the one paper it should become; an expanded entry point into phase 06.
- Peer Review — A coordinated, cutoff-bounded review pipeline that produces structured artifacts for the AI paper reviewer to ground its verdicts in. The Proof Dissection Track is a parallel sub-track for reading a theoretical paper rather than reviewing it (cartography → personalized LaTeX/memoir lecture note).
- Math Brainstorming — An iterative ecosystem of agents for mathematical problem exploration, construction, and synthesis.
- Writing & Documentation — Cross-cutting writing auditors used directly or invoked by paper-writing agents to enforce six orthogonal disciplines across any document register: narrative clarity, epistemic calibration, evidence provenance, citation provenance, theorem presentation, and AI-contribution disclosure.
- Formal Verification — Agents for Lean 4 proof development, validation, and documentation.
The research framework operationalizes both benevolent and hostile reviewer perspectives:
- Benevolent Reviewer: Assumes good faith, looks for signal over perfection, asks "Is there a real idea here?"
- Hostile Reviewer: Assumes overclaiming, searches for gaps and shortcuts, asks "What justifies rejection?"
A phase succeeds when a hostile reviewer cannot identify a fatal flaw and a benevolent reviewer can articulate why the phase adds value.
All 44 agents at a glance. Click an agent name to jump to its detailed description.
| Agent | Purpose |
|---|---|
01-research-framing-validator |
Rigorous problem framing across six dimensions before any implementation |
02-literature-discovery-mapper |
Theory-anchored literature analysis; positioning as necessary not just novel |
03-research-design-auditor |
Convert a framed problem into an auditable plan of inquiry |
04-research-data-architect |
Design, construct, validate, and document data with construct mappings |
05-research-analysis-interpreter |
Convert artifacts into validated findings with robustness testing |
06-argument-architect |
Claim-evidence alignment; 1–3 irreducible claims with articulated limits |
07-paper-structure-architect |
Section-level narrative architecture; concentric arc; progressive elaboration |
08-research-revision-validator |
Close epistemic loopholes; linguistic precision; claim-evidence matrix |
09-research-validation-qa |
Hostile-third-party reproducibility, methodology, and ethics audit |
10-scholarly-submission-strategist |
Venue selection, formatting, archival release, reviewer-response matrix |
| Agent | Purpose |
|---|---|
ai-paper-reviewer |
Dual benevolent/hostile pre-submission review across all ten phases |
arxiv-gap-scanner |
Full-pipeline literature-gap scan against a body of work over an arxiv window |
citation-provenance-auditor |
Citation gate: PID + BibTeX + claim-mapping + canonicality, severity-tiered |
claim-disposition-gate |
Total claim-surface enumeration at results freeze; five-way disposition; ledger + risk register turn re-reviews into lookups |
literature-synthesis-auditor |
Agreement/conflict matrices across sources; consensus extraction; methodological divergence |
research-session-memory |
Indexed cross-session memory: concepts, approaches, negative results, open questions |
scientific-narrative-architect |
Multi-scale narrative architecture across audiences (Nature/Physics/AI conf/Blog) |
venue-archetype-distiller |
Reverse-engineer a venue's success recipe over a window into an archetype + scorecard |
| Agent | Purpose |
|---|---|
research-shaping-orchestrator |
User-callable entry point; sequences divergence → selection → sculpt → phase 06 |
research-divergence-cartographer |
Over-generate 5–12 candidate red threads from a body of work |
red-thread-selector |
Converge on one thread via six-dimension scoring + mandatory mechanism checks |
| Agent | Purpose |
|---|---|
paper-compressor |
Lossless-on-claims compression: tier inventory, methods, datasets, theorem + figure/table indexes, cutoff |
literature-expansion |
Cutoff-bounded prior-art bundle (30–50 works, five role buckets, missing-citation flags) |
baseline-scout |
Independently re-derive expected baselines/datasets, reconcile with reported set |
domain-historian |
Subfield-specific significance rubric; four-stage at-time vs counterfactual verdict |
claim-interrogator |
Per-Tier-1/2-claim verdicts with 3–7 questions and severity tags |
math-review-router |
Routes theorem questions to math-brainstorming agents when theory_heavy: true |
| Agent | Purpose |
|---|---|
proof-dissection-orchestrator |
User-callable entry point; sequences compress → cartography → adversarial → tutor |
proof-chain-cartographer |
Static map: proof DAG, prerequisite-concept inventory, compressed-step inventory |
proof-tutor |
Personalized walkthrough: LaTeX memoir lecture note (default) or live whiteboard |
| Agent | Purpose |
|---|---|
reframer |
8–12 alternative problem encodings via seven transformation types |
perturber |
10–15 nearby variants by modifying assumptions, parameters, constraints |
math-constructor |
5–10 explicit objects/examples via seven construction strategies |
math-strategist |
5–8 proof-search roadmaps without attempting full proofs |
obstructor |
Adversarial stress-test: counterexamples, hidden assumptions, structural impossibilities |
research-director |
Synthesize and prioritize brainstorming outputs into a research portfolio |
| Agent | Audits |
|---|---|
narrative-clarity-auditor |
How the prose reads at the venue's register (eight registers calibrated) |
epistemic-calibration-auditor |
What the prose claims relative to evidence (overclaim + devil's advocate + capability-claim schema) |
evidence-provenance-auditor |
That the evidence chain exists (data → script → figure → claim) |
citation-provenance-auditor |
That cited works are real, canonical, and support the cited claim (gate-enforced; lives in research/tools/) |
theorem-presentation-auditor |
That every theorem has rhythm and every proof has reviewer-skimmable architecture |
ai-contribution-disclosure-auditor |
How the work was produced — assistance ledger, disclosure accuracy, unattributed reuse |
| Agent | Purpose |
|---|---|
lean-proof-chain-validator |
Seven-phase research-grade Lean proof validation, incl. the explicability gate; PASS/CONDITIONAL/FAIL verdict |
lean-proof-frontier-analyzer |
Breadth-first dependency DAG; novelty classification; axiom-boundary documentation |
lean-library-design-auditor |
Post-compile reusability audit — definitions, theorem generality, API, organization; DESIGN-READY / NEEDS-REWORK / NEEDS-DESIGN-DECISION |
Design intent: Describe your goal naturally, and Claude should invoke the right agent proactively.
Examples that trigger automatic invocation:
You: "Review this paper for NeurIPS submission"
→ Claude invokes: ai-paper-reviewer
You: "Check if they compared against the right baselines"
→ Claude invokes: paper-compressor → baseline-scout
You: "These three papers claim different convergence rates - what's going on?"
→ Claude invokes: literature-synthesis-auditor
You: "Help me understand the proofs in this theoretical paper"
→ Claude invokes: proof-dissection-orchestrator
When to be explicit:
- Complex workflows: "Run the full peer-review pipeline on this paper"
- Ambiguous requests: "Build an agreement/conflict matrix for these five papers" (clearer than "analyze the literature")
- Specific features: "Use proof-dissection-orchestrator with tutor_mode: interactive"
- When you know the agent: "Use epistemic-calibration-auditor on this draft"
Best practice: Start natural, get specific if needed.
Map your specific issue to the right agent:
| When You Notice... | Agent to Use | What It Does |
|---|---|---|
| Missing or wrong baselines | baseline-scout |
Independently re-derives expected baselines; flags gaps with severity |
| Conflicting claims across papers | literature-synthesis-auditor |
Builds agreement/conflict matrices; diagnoses methodological divergences |
| Claims stronger than evidence | epistemic-calibration-auditor |
Matches language to evidence strength; devil's advocate on claims |
| Can't trace where numbers came from | evidence-provenance-auditor |
Traces figures/tables/numbers → scripts → data; checks chain integrity |
| Citation seems wrong or unsupported | citation-provenance-auditor |
Verifies DOIs; maps claims to evidence in cited works; checks canonicality |
| Theorem proof feels hand-wavy | math-review-router → math agents |
Routes to reframer/perturber/constructor/strategist/obstructor |
| Unclear if contribution is significant | domain-historian |
Subfield-specific significance rubric; at-time vs. counterfactual verdict |
| Prose is confusing or unclear | narrative-clarity-auditor |
Register-calibrated clarity discipline; flags padding and confusion points |
| Missing key related work | literature-expansion |
Cutoff-bounded prior-art bundle; flags missing citations with severity |
| Theorem presentation is opaque | theorem-presentation-auditor |
Checks rhythm (statement→intuition→operational→consequence); proof architecture |
| Want comprehensive review | ai-paper-reviewer (pipeline mode) |
Dual benevolent/hostile lens across all ten research phases |
| Want to learn the math deeply | proof-dissection-orchestrator |
Produces personalized lecture notes or interactive walkthrough |
| Unsure what to disclose about AI use | ai-contribution-disclosure-auditor |
Builds the assistance ledger; drafts the disclosure statement; flags understatement |
| Result is correct but nobody can explain it | lean-proof-chain-validator (Phase 7) or ai-paper-reviewer (talk test) |
Explicability gate for formal work; talk test for manuscripts |
| Every review round finds a different error | claim-disposition-gate |
Dispositions the whole claim surface once (PROVED/MEASURED/TESTED/HEDGED/CUT); later reviews become ledger lookups |
Scenario: You're reviewing a paper and notice multiple issues.
Natural language approach (recommended first):
You: "I'm reviewing this paper. Here are my concerns:
1. Missing baseline comparisons to Method X
2. Conflicting claims about convergence rates in the related work
3. Figure 2 shows 15% improvement but I can't find the data trail
4. The main theorem's proof sketch is too compressed"
Claude should recognize and invoke:
- Issue 1 →
baseline-scout - Issue 2 →
literature-synthesis-auditor - Issue 3 →
evidence-provenance-auditor - Issue 4 →
math-review-routerortheorem-presentation-auditor
Explicit workflow (when you know what you want):
# Step 1: Get structured claims
Use the paper-compressor agent on paper.pdf
# Step 2: Check baselines
Use the baseline-scout agent on compressed_paper.md
# Step 3: Synthesize literature conflicts
Use the literature-expansion agent on compressed_paper.md
Use the literature-synthesis-auditor agent on prior_art_bundle.md with synthesis_scope: claim-level
# Step 4: Check evidence provenance
Use the evidence-provenance-auditor agent on /path/to/paper-repo with audit_target: paper
# Step 5: Check theorem presentation
Use the theorem-presentation-auditor agent on paper.pdf with register: theoretical-paper
# Step 6: Get comprehensive verdict
Use the ai-paper-reviewer agent on paper.pdf with mode: pipeline| I Want To... | Start With... | Notes |
|---|---|---|
| Review paper before submission | ai-paper-reviewer (pipeline or standalone) |
Pipeline mode runs upstream agents first for grounded verdicts |
| Understand a theoretical paper | proof-dissection-orchestrator |
Produces personalized lecture notes tailored to your background |
| Check specific claim is supported | claim-interrogator or epistemic-calibration-auditor |
Claim-interrogator for systematic per-claim audit; epistemic for devil's advocate |
| Verify baseline comparisons | baseline-scout |
Independently derives what should be there; no anchoring bias |
| Resolve conflicting sources | literature-synthesis-auditor |
Agreement/conflict matrices with methodological divergence analysis |
| Check reproducibility | evidence-provenance-auditor |
Traces every number/figure/table to origin |
| Assess significance | domain-historian |
Field-calibrated rubric; prevents anachronistic judgments |
| Audit theorem proofs | theorem-presentation-auditor + math-review-router |
Presentation auditor for structure; router for soundness |
| Write a paper from scratch | Follow Workflow A (10-phase pipeline) | Or start with specific phase if framing is clear |
| Turn body of work into paper | research-shaping-orchestrator |
Diverges over candidates, then converges on one red thread |
| Remember findings across sessions | research-session-memory |
Index concepts, approaches, negative results, open questions |
| Fix draft clarity issues | narrative-clarity-auditor |
Register-calibrated (blog/paper/lecture-note/etc.) |
| Catch overclaiming | epistemic-calibration-auditor |
Language-to-evidence matching + devil's advocate |
| Gate a paper at results freeze | claim-disposition-gate |
Enumerates and dispositions every claim; emits claim_ledger.md + risk register; mode: delta re-runs only what a revision touched |
Some agents orchestrate others automatically:
ai-paper-reviewer(pipeline mode) → consumes artifacts frompaper-compressor,literature-expansion,baseline-scout,domain-historian,claim-interrogator,math-review-routerresearch-shaping-orchestrator→ sequencesresearch-divergence-cartographer→red-thread-selector→scientific-narrative-architect(sculpt) →06-argument-architectproof-dissection-orchestrator→ sequencespaper-compressor→proof-chain-cartographer→math-review-router(optional) →proof-tutormath-review-router→ delegates toreframer,perturber,math-constructor,math-strategist,obstructorclaim-disposition-gate→ delegates depth checks per disposition:lean-proof-chain-validator(PROVED),evidence-provenance-auditor(MEASURED),obstructor(TESTED),epistemic-calibration-auditor(HEDGED),citation-provenance-auditor(priority claims); owns totality and the ledger itself
When you invoke an orchestrator, the sub-agents run automatically — you don't need to call them individually.
Use research-session-memory for long-running projects:
# After completing a research phase:
Use research-session-memory to index: [findings/approaches/negative results]
# Before starting new work:
Query research-session-memory for: "What have we learned about [topic]?"
# At milestones:
Use research-session-memory to synthesize across sessions: [date range or topic]
This prevents:
- Re-attempting failed approaches
- Rediscovering prior findings
- Losing conceptual continuity across sessions
What are you doing?
│
├─ Writing a new paper
│ ├─ From idea → Follow Workflow A (10-phase pipeline)
│ └─ From body of work → research-shaping-orchestrator
│
├─ Reviewing someone's paper
│ ├─ Comprehensive review → ai-paper-reviewer (pipeline mode)
│ ├─ Specific issues → See "Issue → Agent Quick Reference" above
│ └─ Understanding the math → proof-dissection-orchestrator
│
├─ Auditing your own draft
│ ├─ Overall quality → Run all 6 writing auditors
│ ├─ Clarity issues → narrative-clarity-auditor
│ ├─ Overclaiming → epistemic-calibration-auditor
│ ├─ Missing provenance → evidence-provenance-auditor + citation-provenance-auditor
│ ├─ Theorem presentation → theorem-presentation-auditor
│ └─ What to disclose about AI use → ai-contribution-disclosure-auditor
│
├─ Exploring a math problem
│ └─ Invoke math-brainstorming agents (or research-director to orchestrate)
│
├─ Managing long-running research
│ └─ research-session-memory (index, query, synthesize)
│
├─ Targeting a venue
│ ├─ What does a winning paper here look like? → venue-archetype-distiller
│ └─ Where should I submit / formatting / rebuttal → 10-scholarly-submission-strategist
│
└─ Synthesizing literature
├─ Finding sources → literature-expansion or arxiv-gap-scanner
├─ Understanding conflicts → literature-synthesis-auditor
└─ Verifying citations → citation-provenance-auditor
End-to-end usage patterns. Each workflow names the agents in invocation order; click any agent name above to jump to its detailed spec.
For a fresh research project where the framing is not yet locked.
01-research-framing-validator— define the problem rigorously02-literature-discovery-mapper— position the work; gate cited literature throughcitation-provenance-auditor03-research-design-auditor— convert framing to a testable plan04-research-data-architect— build data with provenance documented end-to-end05-research-analysis-interpreter— analyze with robustness/ablation06-argument-architect— distill 1–3 irreducible claims; the agent's DoD now invokes the writing auditors07-paper-structure-architect— section-level architecture; delegates clarity and theorem-presentation to the auditorsclaim-disposition-gate— results frozen, draft stable: disposition the entire claim surface once; emitsclaim_ledger.md+ risk register08-research-revision-validator— close loopholes against the ledger (delta-only on revision rounds); pairs withepistemic-calibration-auditor09-research-validation-qa— adversarial reproducibility audit of the artifacts behind PROVED/MEASURED/TESTED entries10-scholarly-submission-strategist— venue alignment, formatting, archivalai-paper-reviewer— pre-submission internal review, in ledger mode: findings cite ledger entries or report enumeration failures
scientific-narrative-architect is invoked throughout phases 6–10 for drafting, restructuring, audience adaptation, and quality control.
For accumulated work that needs to converge on a single contribution.
- Author a
body_of_work.mdmanifest (results, theorems, experiments, drafts, abandoned threads, anomalies) research-shaping-orchestrator— sequences divergence → selection → sculpt → phase-06 handoff. Treatsselection_outcome: deferredas a first-class stop, not a failure.- Continue with phases 06–10 as in Workflow A; phase 06 switches from open-ended distillation to validation of the converged claims when
red_thread.mdis present.
For papers whose math is partly outside your comfort zone — produces a personalized lecture note.
proof-dissection-orchestrator— single entry point. Sequences:paper-compressor(precondition; reused if present)proof-chain-cartographer(always; emits proof DAG, concept inventory, compressed-step inventory)math-review-router(auto-conditional; soundness audit when plausibility flags fire)proof-tutorin document mode (default) — generateslecture_notes.tex(memoir, Feynman style, distill-inspired explainer layout) tailored to your knowledge profile
- Knowledge profile at
~/.claude/projects/<project>/memory/theoretical-paper-knowledge-profile.mdcarries forward across papers — concepts you confirmed once are skipped on the next paper.
Variants: tutor_mode: interactive for a live whiteboard session; tutor_style: classic for dense memoir without distill extensions; stage: cartography to stop after the static map.
For pre-submission internal review or external peer review.
paper-compressor— extract claims, evidence, baselines, theorem index, cutoff dateliterature-expansion— cutoff-bounded prior-art bundle; gates citations throughcitation-provenance-auditorbaseline-scout— independently re-derive expected baselines, flag gapsdomain-historian— subfield-specific significance rubric and at-time verdictclaim-interrogator— per-claim verdicts grounded in upstream artifactsmath-review-router(iftheory_heavy: true) — routes theorem audits to math-brainstorming agentsai-paper-reviewer— dual benevolent/hostile lens grounded in the upstream artifacts
If the reviewer also wants to understand the paper's proofs deeply, run Workflow C in parallel for the lecture-note artifact.
For any draft (paper, lecture note, blog post, tech report, status report). Run the writing auditors that apply at the chosen register; they cover orthogonal concerns and can run in any order:
narrative-clarity-auditor— register-calibrated clarity disciplineepistemic-calibration-auditor— overclaim/underclaim + devil's advocateevidence-provenance-auditor— chain integrity for data and numerical claimscitation-provenance-auditor— citation gate, severity-tieredtheorem-presentation-auditor— theorem rhythm + modular proof architecture (paper/lecture-note registers)ai-contribution-disclosure-auditor— assistance ledger, disclosure accuracy, unattributed reuse
A paper that passes all six is reproducible, defensible, honest about what it claims, honest about how it was made, and structured for the reviewer to triangulate at a glance.
For deciding how to shape (or where to send) a paper, using what actually succeeds at the venue.
venue-archetype-distiller— profile the venue's high-performers in your subfield over a window (default 5y); emitsarchetype.md(the recipe) +scorecard.md(the rubric), and optionallyour_score.md+recipe_handoff.mdscientific-narrative-architect— load the archetype as its optional ARCHETYPE input and Draft/Restructure/Adapt/Sculpt the paper toward the recipe, surfacing any conflict with its own clarity/claim discipline10-scholarly-submission-strategist— if the distiller reveals the subfield is a poor fit for the venue, use its finding to reconsider the targetai-paper-reviewer— usescorecard.md's must-pass gates as an additional pre-submission checklist
Run step 1 once per candidate venue and diff the archetypes when choosing between venues.
agent-specs/
├── README.md
├── agents/
│ ├── research/
│ │ ├── phases/ # Sequential research workflow (10 phases)
│ │ │ ├── 01-research-framing-validator.md
│ │ │ ├── 02-literature-discovery-mapper.md
│ │ │ ├── 03-research-design-auditor.md
│ │ │ ├── 04-research-data-architect.md
│ │ │ ├── 05-research-analysis-interpreter.md
│ │ │ ├── 06-argument-architect.md
│ │ │ ├── 07-paper-structure-architect.md
│ │ │ ├── 08-research-revision-validator.md
│ │ │ ├── 09-research-validation-qa.md
│ │ │ └── 10-scholarly-submission-strategist.md
│ │ ├── tools/ # Cross-phase utility agents
│ │ │ ├── ai-paper-reviewer.md
│ │ │ ├── arxiv-gap-scanner.md
│ │ │ ├── citation-provenance-auditor.md
│ │ │ ├── claim-disposition-gate.md
│ │ │ ├── literature-synthesis-auditor.md
│ │ │ ├── research-session-memory.md
│ │ │ ├── scientific-narrative-architect.md
│ │ │ └── venue-archetype-distiller.md
│ │ ├── peer-review/ # Coordinated review pipeline (artifacts → ai-paper-reviewer)
│ │ │ ├── paper-compressor.md
│ │ │ ├── literature-expansion.md
│ │ │ ├── baseline-scout.md
│ │ │ ├── domain-historian.md
│ │ │ ├── claim-interrogator.md
│ │ │ ├── math-review-router.md
│ │ │ ├── proof-dissection-orchestrator.md # Proof-dissection track (parallel to review pipeline)
│ │ │ ├── proof-chain-cartographer.md
│ │ │ └── proof-tutor.md
│ │ └── shaping/ # Diverge → converge: pick the paper hiding in a body of work
│ │ ├── research-shaping-orchestrator.md # User-callable entry point
│ │ ├── research-divergence-cartographer.md
│ │ └── red-thread-selector.md
│ ├── math-brainstorming/ # Iterative problem exploration ecosystem
│ │ ├── reframer.md
│ │ ├── perturber.md
│ │ ├── math-constructor.md
│ │ ├── math-strategist.md
│ │ ├── obstructor.md
│ │ └── research-director.md
│ ├── writing/ # Cross-cutting writing tools (any document type)
│ │ ├── narrative-clarity-auditor.md
│ │ ├── epistemic-calibration-auditor.md
│ │ ├── evidence-provenance-auditor.md
│ │ ├── theorem-presentation-auditor.md
│ │ └── ai-contribution-disclosure-auditor.md
│ └── formal-verification/
│ └── lean/ # Lean 4 proof tools
│ ├── lean-proof-chain-validator.md
│ ├── lean-proof-frontier-analyzer.md
│ └── lean-library-design-auditor.md
├── scripts/
│ ├── sync-agents.sh # Symlink agents into ~/.claude/agents/
│ └── lint-descriptions.sh # Enforce DESCRIPTION-STYLE.md (--stats for token load)
└── DESCRIPTION-STYLE.md # Frontmatter-description conventions (budgets, template, examples)
Frontmatter description: fields are loaded into every Claude Code session and drive
agent routing; they follow the template, budgets, and example policy in
DESCRIPTION-STYLE.md, enforced by scripts/lint-descriptions.sh.
The 10-phase workflow takes a research idea from initial framing through publication. Each phase produces specific artifacts and has explicit completion criteria.
Ensures research problems are rigorously defined and properly scoped before any implementation begins. Evaluates framing across six dimensions: big picture motivation, opportunity identification, solution space exploration, implications, opportunity landscape ranking, and definition-of-done criteria. Rejects buzzword-driven framing and requires first-principles reasoning with explicit separation between theory and empirics.
Conducts systematic, theory-anchored literature analysis to position research as addressing necessary gaps rather than merely novel extensions. Performs epistemic triangulation by mapping conceptual, methodological, and empirical landscapes. Identifies where first principles are violated and assumptions are accidents rather than necessities, producing a positioning statement explaining why the problem remains unsolved.
Converts well-framed problems into testable, auditable plans of inquiry. Addresses five pillars — method selection, variables/constructs, data strategy, evaluation metrics, and ethics/reproducibility — ensuring an independent researcher could execute the study without clarification. Applies the meta-success test: can the design fail, would success be believed, would failure be informative?
Designs, constructs, validates, and documents research data and benchmarks with defensible construct mappings. Bridges hypothesis and evidence by creating construct tables mapping theory to observables, designing collection protocols with sampling justification, and performing quality assurance including schema consistency, leakage detection, and edge case analysis. Documents provenance end-to-end.
Converts prepared artifacts into validated findings and defensible insights. Answers four questions: Does the hypothesis hold? Under what assumptions and regimes? Why do results look this way? What survives stress-testing? Rigorously separates demonstrated findings from suggested insights from speculation, with comprehensive robustness testing, ablation studies, and sensitivity analyses.
Transforms validated results into coherent, defensible academic arguments. Enforces claim-evidence-qualification alignment where every central claim has necessary and sufficient evidence, clear scope conditions, and reasoned explanations for why competing interpretations are less plausible. Distills contributions into 1-3 irreducible claims with articulated limitations across theoretical assumptions, regime boundaries, and external validity.
Enforces rigorous narrative architecture where every section answers four core questions (Why exists, What gap, How addressed, So what). Applies concentric narrative arc and progressive elaboration: abstracts compress the entire argument, introductions mirror the abstract at higher resolution, methods make the solution feel unavoidable, and results test claims rather than showcase experiments.
Converts correct papers into convincing, defensible, and reproducible ones by closing epistemic loopholes and enforcing traceability. Constructs claim-dependency graphs, enforces linguistic precision (mapping "show" to prove/demonstrate, quantifying "significant"), builds claim-evidence matrices, audits citations for provenance and scope, and reviews visual artifacts for reproducibility.
Validates work for reproducibility, methodological soundness, ethical compliance, and scholarly integrity. Approaches validation as a hostile but competent third party: "Where would an adversary succeed in invalidating this?" Evaluates three reproducibility levels (internal, external, conceptual) and treats ethical review as a threat model examining data provenance, privacy, bias, and deployment constraints.
Transforms research artifacts into durable scholarly contributions through strategic venue selection, rigorous formatting, and controlled release. Classifies papers on three axes (contribution type, evaluation mode, temporal relevance) for venue alignment. Ensures archival integrity with versioned releases and immutable identifiers. Creates structured response matrices for reviewer feedback.
Domain 6 — post-acceptance digestion. Publication sits in the middle of a longer chain (generation → verification → exposition → publication → digestion → canonicalization) in which value accrues to the right while effort concentrates to the left. A published result nobody incorporates has completed the cheap half of its journey. The phase therefore emits digestion_plan.md alongside the submission package: the expert talk outline, a short expository form carrying the idea without the apparatus, the canonical statement (the result as a later survey would state it, stripped of this paper's framing — a result that resists compact restatement usually has an unresolved conceptual boundary, and finding that out before publication is cheap), the artifact-upstreaming path (mathlib PR, library contribution, benchmark submission), the process record, the AI-assistance disclosure statement, and specific reciprocity commitments. It closes on a gate adopted from Tao: if the authors cannot convincingly demonstrate that they can give a clear, expert-level talk on their results — correct, and properly attributed — the result should not be published. Three disqualifying signatures: they can state the result but not explain why it is true; they can reproduce the argument but cannot say which step carries the difficulty; they cannot attribute the components. None is fixed by more polish.
These agents can be invoked at any point during the research workflow.
Conducts rigorous pre-submission internal reviews using a dual-perspective framework. Evaluates papers across all ten research phases, applying both benevolent and hostile reviewer lenses simultaneously. Identifies fatal flaws that would trigger immediate rejection, provides a prioritized revision roadmap, and issues a conference-readiness score calibrated to top-tier venue acceptance rates (~20-25%).
The talk test. The phase framework can be satisfied piecewise by a paper nobody can explain, so a paper-level gate runs after the phase reviews: could the authors give a clear, expert-level talk on this result — correct, and properly attributed? The reviewer reconstructs four things from the manuscript alone: the one idea in a paragraph (the mechanism, not the pipeline); where the difficulty lives and what breaks without it; what is borrowed and from whom; and the first question a knowledgeable listener would ask that the paper leaves open. Verdict TALK-READY or TALK-INCOMPLETE, reported beside the phase verdicts rather than folded into them — it is possible, and increasingly common, for a paper to be correct, well-formatted, adequately evidenced and still unabsorbable, and the phase framework will pass it.
Orchestrates a seven-phase literature-gap scan against a body of work — paper directory, formal-verification module, or research roadmap — over a defined arxiv window. Generates stream-specific queries from open theorems, bulk-fetches abstracts on the main thread (subagents are sandboxed from network), shards triage across parallel 02-literature-discovery-mapper instances, downloads PDFs under a hard cap, deep-reviews the critical tier (per-paper claim catalogs and reuse plans via 05-research-analysis-interpreter or lean-proof-chain-validator), and synthesises a deadline-sorted action list with an Impact × Effort × Stream matrix. Emits a working scan directory (anchor.md, raw/, tracks/, pdfs/, reviews/, scan.md, optional roadmap_delta.md) rather than a single report. Distinct from 02-literature-discovery-mapper (single-pass landscape mapping) by running the full pipeline including PDF download and per-paper deep review.
Performs comprehensive citation audits: establishes persistent identifiers (DOI, arXiv, ISBN), verifies BibTeX entries against authoritative sources (Crossref, arXiv, PubMed, DBLP) with field-by-field diffs, maps every citation occurrence to specific claims with evidence pointers and support strength, and assesses canonicality (peer-reviewed over preprint, primary over secondary). Generates provenance files per citation key and TeX annotation comments.
Runs once, at results freeze, and dispositions the paper's entire falsifiable-claim surface: every claim across the theory, empirical, and interface zones gets exactly one of five dispositions — PROVED (machine-checked, ledger reference at a pinned commit), MEASURED (pipeline-produced, script + data provenance), TESTED (falsification attempted and survived, artifact kept), HEDGED (prose scoped to exactly what is established), or CUT. The undispositioned residue is emitted as the risk register — the exact set of places a reviewer will strike. Narrative claims (mechanism talk, explanatory and naturalness assertions) are dispositioned via internally constructed shadow statement pairs — the strongest statement the prose commits to (S⁺) vs. the weakest the argument needs (S⁻), with working definitions on demand — audit apparatus that never obligates the paper to display the formalism, but makes hedging, testing, and calibration well-posed and flags cheap promotions to formal results. A carrier map couples every claim to the figures and tables that carry it and every artifact back to its claims — schematics are dispositioned for the structure they commit the method to — so claims and their visuals are reviewed together and orphans in either direction are findings. Enumeration is verified against an eight-failure-mode × three-zone grid (satellite claims, constant drift, statement drift, vacuity, universal claims, unverified computation, positioning, edge omission — each with a theory, empirical, and interface face), and a ten-step gate runs in priority order: five prevention rules (generate don't transcribe; non-vacuity by construction; every-regime statements; single source of truth across the theory↔empirics boundary; freeze-or-regenerate verified prose), three mechanical passes (numeric spot-checks and parameter sweeps; intra-paper cross-reference audit; quantifier lint), and two human passes (framing counterexample hunt; individually verified priority claims).
The design premise: review rounds recur because each reviewer samples a different slice of an unenumerated claim space. Disposition the whole surface once and later reviews become lookups — 08-research-revision-validator verifies the manuscript against the ledger and audits only revision deltas, 09-research-validation-qa validates the artifacts behind the dispositions, and ai-paper-reviewer reviews by ledger lookup, reporting any claim missing from the ledger as an enumeration failure. Depth checks are delegated (lean-proof-chain-validator for PROVED, evidence-provenance-auditor for MEASURED, obstructor for TESTED, epistemic-calibration-auditor for HEDGED, citation-provenance-auditor for priority claims); the gate owns totality and the ledger. mode: delta re-dispositions only the claims a revision touches. Distinct from claim-interrogator (verdicts on someone else's paper under review) — this gate dispositions your own paper's surface before packaging.
Analyzes collections of papers to identify consensus, conflicts, and gaps. Builds agreement/conflict matrices showing where sources align vs. diverge on specific claims, performs methodological divergence analysis to diagnose why different papers report different results (datasets, metrics, assumptions), flags conflicting claims with severity levels (critical/high/medium/low), and produces synthesis recommendations for related work sections and baseline comparisons. Companion to literature-expansion (which finds sources) and citation-provenance-auditor (which verifies citations) — this agent synthesizes what the sources collectively say. Detects anti-patterns including circular citation chains, citation drift, scope elision, and definitional inconsistencies. Outputs include claim inventory, agreement matrices, conflict analyses with probable causes, consensus positions with citation recommendations, and gap maps.
Builds, queries, and maintains indexed knowledge structures across research sessions. Organizes memory into five indexes: conceptual understanding (evolving definitions and cross-references), approaches and strategies (both successful and failed, with failure modes), negative results (failed experiments and disproven conjectures as first-class outputs), open questions (unresolved threads with blockers and priorities), and cross-session synthesis (milestone integrations). Each memory includes session provenance, cross-links to related memories, and lifecycle management (active/superseded/archived). Enables future sessions to build on prior understanding rather than rediscovering findings, prevents re-attempting failed approaches, and maintains investigative trail continuity. Distinct from code-level memory, citation provenance, and evidence provenance — this captures the conceptual understanding and research trajectory across the long arc of a project.
Constructs scientific writing achieving causal intelligibility at every scale, optimized for mathematically oriented ML venues (NeurIPS theory, COLT, AISTATS, JMLR) as well as Nature/Science and physics/math journals. Beyond clarity, enforces scientific strategy through three interlocking frameworks: a three-tier claim architecture (core/supporting/peripheral) with explicit scope containment; the Three Axes of Contribution model (Theory/Method/Evaluation) requiring axis dominance declaration, alignment verification, and venue-specific coverage; and Single Mechanism Architecture ensuring all results derive from one central mechanism (structural principle + mathematical representation + observable consequences). Also enforces narrative tension, theorem–empirical alignment, contribution compression (≤ 5 named objects), figure architecture (four roles), a three-layer reading model, reviewer adversary simulation, and Feynman-style clarity at every scale. Accepts an optional ARCHETYPE input (archetype.md / recipe_handoff.md from venue-archetype-distiller) as venue-calibrated guidance layered on top of its rules, surfacing conflicts to the user rather than silently overriding its own clarity and claim discipline.
Reverse-engineers what a successful paper looks like at a specific venue over a time window (default 5 years) and packages it as a reusable recipe. Enumerates the venue's papers in the window filtered to the user's subfield, enriches them with age- and field-normalized impact metrics (OpenAlex citation_normalized_percentile / fwci, Semantic Scholar influentialCitationCount, optional altmetrics) blended with venue accolades (oral/spotlight/best-paper/test-of-time), and selects top exemplars alongside a same-venue baseline-contrast sample. Downloads and structurally dissects each exemplar (via paper-compressor / 07-paper-structure-architect subagents) into a per-paper fingerprint — title pattern, abstract shape, opening move, claim architecture, section rhythm, evidence portfolio, figure strategy, positioning, register. Distills two artifacts: archetype.md (invariants separated from variance bands and anti-patterns, each invariant carrying its exemplar-vs-baseline lift, with mandatory survivorship/causation caveats) and scorecard.md (a weighted, self-assessable rubric with must-pass gates). Optionally scores the user's draft and emits a recipe_handoff.md for scientific-narrative-architect. Works for AI conferences and journals. All metric fetching and PDF pulling is main-thread (subagents are sandboxed from network); metric honesty is absolute (unknown over fabrication) and cross-cohort raw-count comparison is forbidden. Distinct from arxiv-gap-scanner (scans what threatens a program), 02-literature-discovery-mapper (positions your work), and domain-historian (calibrates significance of one paper under review) — this agent profiles the venue's winners to produce a construction template.
The anti-Goodhart clause (Phase 6b, mandatory). The scorecard is the most dangerous artifact this agent produces, and the danger is intrinsic: when a measure becomes a target, it ceases to be a good measure. A rubric distilled from past winners describes what correlated with success in a window; optimized against directly, it selects for the surface features that were evidence of good work and against the work itself — and the better the distillation, the more efficiently that failure becomes available. Every scorecard.md therefore opens with a clause stating that the scorecard is a diagnostic and not an objective (a low score locates something worth examining; a high score is not an achievement), that each dimension names the property it proxies for so score-versus-property disagreement is detectable, that the score describes a window and venues drift, and that fixing a criterion by adding the surface feature it measures scores points and improves nothing. When scoring a draft, criteria that score well while the underlying property is unmet are listed above the ordinary gap list — they are invisible to the author and obvious to a reviewer.
A research project rarely has one obvious paper inside it. Bodies of work accumulate results, theorems, experiments, abandoned threads, and surprising observations — and the temptation is to cram all of it into one dense paper with multiple mechanisms and unfocused contributions. The shaping layer addresses this by deliberately diverging over candidate paper-framings before converging on one, then sculpting the body of work down to the single red thread that becomes the paper.
This layer is an expanded entry point into phase 06 (argument-architect), not a replacement. Phase 06 already validates and scopes claims that have been chosen; the shaping layer chooses them.
body_of_work.md (user-authored manifest)
│
▼
research-shaping-orchestrator (user-callable entry point; sequences the four stages below)
│
▼
research-divergence-cartographer ──► candidate_threads.md (5–12 threads, deliberately over-generated)
│
▼
red-thread-selector ──► red_thread.md (1 chosen + runners-up + score table; or selection_outcome: deferred)
│
▼
scientific-narrative-architect ──► sculpt_plan.md (keep / move-to-appendix / cut)
(mode: Sculpt; auto-conditional)
│
▼
06-argument-architect (existing) — validates the converged claims;
open-ended distillation is replaced by validation
when red_thread.md is present.
If no shaping artifacts are produced, phase 06 behaves exactly as it does today.
User-callable entry point. Sequences the four stages, enforces preconditions at every handoff, handles selection_outcome: deferred as a first-class outcome rather than retrying with relaxed thresholds, and supports stop-early flags (diverge | select | sculpt | argue) and resume-at-stage when prior artifacts are valid. Auto-conditional sculpting: invokes Sculpt Mode whenever a draft is provided, or whenever body_of_work.md lists ≥ 1 abandoned thread, decorative experiment, or off-axis result. Hands off to 06-argument-architect with red_thread.md and (if produced) sculpt_plan.md so phase 06 switches from open-ended distillation to claim validation.
Invocation:
# Full pipeline through phase-06 handoff
Use the research-shaping-orchestrator agent on body_of_work.md
# Stop after selection so you can review before sculpting
Use the research-shaping-orchestrator agent on body_of_work.md with stage: select
# Sculpt against an existing complete draft, reusing red_thread.md from a prior run
Use the research-shaping-orchestrator agent on body_of_work.md with stage: sculpt, draft: paper_draft.tex
# Skip sculpting and hand off directly to phase 06
Use the research-shaping-orchestrator agent on body_of_work.md with sculpt: off
The orchestrator emits shaping_handoff.md recording which stages ran, the selection outcome (selected or deferred with diagnosis), the sculpt decision basis, and any conditional findings phase 06 should address.
First stage. Reads a user-authored body_of_work.md manifest (results, theorems, experiments, datasets, prior drafts, open threads, abandoned attempts, anomalies) and over-generates 5–12 candidate red threads spanning ≥3 distinct novelty types and ≥2 distinct contribution axes. Each thread carries a structured yaml block: core tension, possible core claim, supporting claim sketches, evidence pointers, missing evidence, novelty type, contribution axis, venue fit, risk, significance hypothesis. The agent does not rank, recommend, or favor; selection is downstream. Anti-convergence guardrails prevent synonym-threads, risk-laundering, and pre-ranking.
Convergence stage. Scores every candidate on six dimensions (novelty, clarity, technical depth, significance, evidence sufficiency, narrative inevitability) and applies six penalties (density, claim sprawl, mixed mechanisms, multi-axis dominance, decorative experiments, unsupported ambition). Mandatory pass/fail mechanism checks — Paper Identity Test and Single Mechanism Test (both from scientific-narrative-architect) — apply before scoring; threads that fail either cannot be selected. The selector simulates the dual benevolent/hostile reviewer lens internally per candidate (vocabulary borrowed from ai-paper-reviewer, not invoked) and produces an auditable red_thread.md with the chosen thread, 2–3 runners-up with disqualifying gaps, rejected threads with reasons, and the full scoring table. If no thread passes the mandatory checks, the agent returns selection_outcome: deferred rather than forcing a choice.
Distinction from research-director: research-director (under agents/math-brainstorming/) portfolios research directions across novelty / feasibility / insight / risk / tool-availability — its target is a research program. red-thread-selector picks one paper to write now from a body of work that already exists — its target is a single artifact. The two live in different stages of the research lifecycle.
Sculpting is a new mode of scientific-narrative-architect, not a separate agent. Sculpt Mode reads red_thread.md plus the body of work (or a complete draft), re-validates the Paper Identity and Single Mechanism Tests, and applies the Remove-the-Mechanism Test at the element level to every result, theorem, figure, experiment, and derivation. Each element is classified into keep, move_to_appendix, or cut, with a one-line justification grounded in mechanism preservation or contribution-axis alignment. The default is cut, not appendix; the appendix is for genuinely supportive material, not a holding pen for material the author cannot bear to remove. The output, sculpt_plan.md, hands off cleanly to phase 06 for argument validation.
- You have months of accumulated work and need to decide which paper it should become.
- A draft has grown dense and unfocused; sculpting can identify what is load-bearing.
- Multiple candidate framings are competing in your head and you want them on the page side-by-side.
When the framing is already obvious, skip the shaping layer and start at phase 06.
The peer-review agents form a coordinated pipeline that produces structured artifacts the ai-paper-reviewer consumes in its Pipeline Mode. Unlike the math-brainstorming ecosystem, ordering matters: each agent depends on artifacts from the agents upstream of it. The pipeline addresses the failure modes of single-prompt review — anachronistic prior-art, missing baseline scouting, ungrounded significance verdicts, and theory-paper math gaps.
paper-compressor ──► compressed_paper.md
│
├──► literature-expansion ──► prior_art_bundle.md
│ │
│ └──► (hands bibkeys to) citation-provenance-auditor
│
├──► domain-historian ──► significance_rubric.md
├──► baseline-scout ──► baseline_gap_report.md
├──► claim-interrogator ──► interrogation_log.md
└──► math-review-router* ──► math_review_bundle.md
(* iff theory_heavy=true; delegates to math-brainstorming agents)
│
▼
ai-paper-reviewer (Pipeline Mode)
— dual benevolent/hostile lens grounded in upstream artifacts
First stage. Converts a paper into a precise, lossless-on-claims artifact: Tier-1/2/3 claim inventory with verbatim quotes and section pointers, method skeleton, exhaustive datasets/baselines/metrics tables, paper-stated and implicit assumptions, theorem index, and an inferred cutoff_date_inferred that bounds all downstream prior-art search. Issues no judgments — pure extraction with traceability.
Constructs a cutoff-bounded prior-art bundle of 30–50 works across five role buckets: foundational, dataset, SOTA, direct competitor, survey. Hard temporal discipline: no work published after cutoff_date_inferred enters the bundle without an explicit exception. For every retrieved work, sets a missing_from_paper flag with severity (critical / expected / helpful), producing the Missing-Citation Report. Hands bibkeys to citation-provenance-auditor for metadata verification rather than duplicating that work.
The highest-impact stage for empirical-claim review. Runs a strict two-pass protocol: Pass 1 independently re-derives the expected datasets and baselines from task and metric without anchoring on the paper's framing; Pass 2 reads the reported set; reconciliation produces a severity-tagged gap report. For each critical or expected gap, names the specific pre-cutoff SOTA reference that should have been compared against and quotes the paper's stated rationale (or no-rationale). Anti-anchoring discipline includes explicit restart conditions.
Calibrates the significance verdict. Names the specific subfield, sketches its history as 3–7 inflection points up to cutoff, enumerates open problems the field considered live as of cutoff, and defines a subfield-specific Tier-1/2/3 contribution rubric. Issues a four-stage calibration verdict (stated → earned → counterfactual at earlier and later dates → final tier) with stage ordering enforced to prevent counterfactual contamination of the at-time judgment. Distinct from scientific-narrative-architect: that agent helps writers; the historian helps reviewers.
For every Tier-1 and Tier-2 claim, generates 3–7 specific questions targeting the weakest defensible point, answers each with paper-internal evidence + external evidence (prior_art_bundle, baseline_gap_report, math_review_bundle), and issues a per-claim verdict (Supported / Partial / Unsupported / Contradicted) with severity (fatal / major / minor / none). Maintains a flat discrepancy log of every observed disagreement between paper-internal and external evidence. Becomes the evidentiary basis the final reviewer cites.
Activates when theory_heavy: true. Re-validates the gate, restates each Tier-1 theorem with assumptions named, and routes targeted questions to the math-brainstorming agents:
reframer: Is the formalization right? Are alternate encodings missed?perturber: Which assumptions are essential? Where does the result fail under relaxation?math-constructor: Counterexamples or boundary cases for Tier-1 theorems?math-strategist: Are proof dependencies plausible? Hand-waved steps?obstructor: Adversarial stress-test of theorems and proof technique.
Preserves delegate outputs in their native formats; the synthesis section consolidates without re-judging.
- Cutoff date is the contract: every downstream agent respects
cutoff_date_inferred. Anachronism is a category-level failure. - Artifacts are explicit: each agent produces one canonical markdown file consumed by name. No implicit hand-offs.
- Severity calibration is shared:
critical/fatallevels propagate acrossprior_art_bundle.md(missing-citation severity) →baseline_gap_report.md(gap severity) →interrogation_log.md(verdict severity) →ai-paper-reviewer(fatal-flaw enumeration). - Graceful degradation: missing artifacts don't silently disable phases of the final review — they are flagged.
A parallel track to the peer-review pipeline, intended for reading a theoretical paper rather than reviewing it. When the math is outside your comfort zone — unfamiliar techniques, citations to results you don't know, hand-waved compressed steps — this track produces a static map of the paper's proof architecture and then converts it into a personalized lecture note (LaTeX, memoir class, Feynman style), or walks you through it interactively. Either way, only background you actually lack gets taught, and what you confirm carries forward across papers.
paper (PDF / arxiv id)
│
▼
paper-compressor ──► compressed_paper.md (precondition; reused if present)
│
▼
proof-chain-cartographer ──► proof_chain.md (DAG over theorems / lemmas / external citations)
concept_inventory.md (prerequisite concepts, per subfield, with difficulty)
compressed_steps.md (every "clearly" / "by standard arguments", flagged)
│
├──► math-review-router (optional, auto-conditional) ──► math_review_bundle.md
│
▼
proof-tutor — three modes:
document (default) ──► lecture_notes.tex (LaTeX memoir, Feynman style; one batched probing round)
interactive ──► live whiteboard session in main conversation
hybrid ──► interactive walk + lecture_notes.tex accumulated in parallel
— reads/writes a persistent knowledge profile so the next paper skips what you already know
User-callable entry point. Sequences the four stages, enforces preconditions at every handoff, and supports stop-early flags (compress | cartography | adversarial | tutor) and a tutor_mode flag (document | interactive | hybrid, default document). Reuses compressed_paper.md if already produced; auto-invokes math-review-router only when the cartographer raises ≥ 5 plausibility flags or any Tier-1 theorem has compressed steps with uncertain certainty (or when the user opts in explicitly). Hands off to proof-tutor in the main conversation rather than spawning it as a subagent — even in document mode the tutor needs the main conversation for a single batched probing round before generating LaTeX.
One-shot map builder. Walks the paper front-to-back, creates one node per numbered/named result with role / formal statement / informal restatement / dependencies (in-paper, external, background concept), and produces a topological ordering of prerequisite concepts grouped by subfield. Light plausibility flags (notation overloading, quantifier-order changes, unstated regularity conditions) are surfaced as side-output; adversarial review is delegated to math-review-router. The cartographer does not teach.
Personalized walkthrough generator. Default mode (document) produces lecture_notes.tex — a LaTeX memoir-class lecture note written in Feynman style: motivation precedes technique, concrete precedes abstract, every proof is told first as a story (the trail of thought) and then formally (the rigorous version). Concepts marked known in the profile appear only in a compact "Concepts assumed familiar" list; concepts marked teach get full Feynman-style tutorials; uncertain compressed steps surface in each theorem's "Loose ends" section and in a "Questions for the authors" appendix. Probing happens once, batched, before generation. interactive mode runs a live whiteboard session in the main conversation; hybrid does both. Reads and writes a persistent knowledge profile at ~/.claude/projects/<project>/memory/theoretical-paper-knowledge-profile.md so subfield fluency, per-concept ledger entries, and open loops carry forward across papers.
Two styles for the LaTeX output (selectable via tutor_style on the orchestrator or style on direct invocation):
explainer(default): distill.pub-inspired layout — wide right margin for sidebars, layered/progressive TikZ figures (comic-strip panels showing how an object is built up), annotated equation arrays where each derivation line carries a margin annotation explaining the move, per-chapter\conceptMapshowing this chapter's slice of the proof DAG with the current theorem highlighted,\anatomyDiagramfor new concept introductions,\counterexampleSketchmargin figures for boundary cases, and\comparativeDiagramfor the multiple-angles narrative-clarity rule. Built on a TikZ template library (seven named macros) and a unifiedtutor-stylepreset so figure quality stays consistent — the agent does not invent ad-hoc TikZ for diagram types the library covers. Optionalhanddrawn: truesub-flag applies a sketchy hand-drawn aesthetic viadecoration={random steps}.classic: dense memoir-class lecture note with conventional figure/equation handling. No margin sidebars, single appendix-only DAG. Use when the reader prefers a denser, more book-like format.
The narrative discipline does not change between styles. Only the layout, figure vocabulary, and margin treatment differ.
The orchestrator is the entry point. Invoke it via the Agent tool with the paper as input:
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf
By default it runs the full pipeline and produces lecture_notes.tex. Common variants:
# Live whiteboard session instead of LaTeX output
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with tutor_mode: interactive
# Both — interactive walk plus LaTeX accumulated in parallel
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with tutor_mode: hybrid
# Classic dense memoir output instead of distill-style explainer
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with tutor_style: classic
# Hand-drawn / sketchy TikZ aesthetic for a warmer tutorial
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with tutor_style: explainer, handdrawn: true
# Stop after the static map; no tutoring, no LaTeX
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with stage: cartography
# Force adversarial soundness review
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with adversarial: on
# Skip adversarial review entirely
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with adversarial: off
# Resume in a later session — re-invoke with stage: tutor; cartography artifacts and knowledge profile
# from the prior session are reused; the tutor resumes at the next undelivered node
Use the proof-dissection-orchestrator agent on /path/to/paper.pdf with stage: tutor
The orchestrator emits dissection_handoff.md recording which stages ran, which were skipped, why, the chosen tutor_mode, and the expected deliverable. After handoff, the tutor either generates lecture_notes.tex (document mode) or walks you through the proofs in your main conversation (interactive/hybrid).
- You're tasked with reviewing a paper whose proof techniques are partly outside your subfield.
- You want a hyper-personalized lecture note for a paper rather than a generic survey of its area.
- You'd rather invest time once in learning the prerequisite concepts (and have that investment compound across future papers) than re-derive them every time.
When the paper's math is fully within your comfort zone, skip this track and use the standard peer-review pipeline.
These agents form an iterative ecosystem (not a linear pipeline). They can be invoked in any order and their outputs feed into each other. The research-director orchestrates and prioritizes outputs from the other five.
Discovers alternative problem encodings that unlock different toolsets. Applies seven transformation types (representation shift, perspective shift, granularity shift, dualization, embedding, relaxation, encoding transformation) to generate 8-12 substantially different reframings. Core insight: breakthroughs often come from a changed viewpoint rather than a new technique. Does not solve problems — transforms them into forms where solutions become tractable.
Maps problem neighborhoods by systematically modifying assumptions, parameters, and constraints. Extracts all assumptions from a problem, then generates 10-15 nearby variants via weakening, strengthening, extremal cases, randomization, and degeneration. Reveals which assumptions are essential vs dispensable, where phase transitions occur, and which variants are easier to attack. Constructs a perturbation landscape matrix identifying the most informative directions.
Builds explicit mathematical objects, examples, and constructions satisfying problem constraints. Applies seven construction strategies (example mining, parametric, incremental, hybrid composition, algorithmic, symmetric/extremal/random) to produce 5-10 diverse candidates. Evaluates constraint satisfaction for each, identifies structural patterns and invariants, and proposes general construction schemas. Constructions serve as evidence for strategists, test cases for obstructors, and empirical foundation of insight.
Designs structured proof-search roadmaps without attempting full proofs. Selects among proof paradigms (induction, contradiction, probabilistic method, spectral, compactness, extremal, algebraic, topological), decomposes problems into dependency trees with difficulty assessment, and generates 5-8 genuinely different strategies with concrete proof plans and required lemmas. Ranks strategies by feasibility and recommends a path. Emulates experienced research mathematicians planning attacks before writing.
Stress-tests ideas, conjectures, and proof strategies by searching for counterexamples, hidden assumptions, and structural impossibilities. Applies six adversarial strategies (counterexample construction, minimal obstruction analysis, hidden assumption detection, adversarial perturbation, boundary stress testing, logical gap detection). Generates 5-8 adversarial instances, isolates root causes explaining why ideas fail, and suggests minimal repairs. Issues verdicts: Fatal, Wounded, or Robust.
Synthesizes, deduplicates, evaluates, and prioritizes research ideas from all brainstorming agents into a structured portfolio. Extracts core mechanisms from candidates, clusters by underlying structure (not surface wording), scores on novelty/feasibility/insight potential/tool availability/failure risk, and classifies into priority tiers: immediate experiment (hours), promising direction (days), high-risk research (weeks+), or discarded. Designs concrete next actions specific enough for execution without clarification.
Typical workflow: Reframer/Perturber explore the space → Constructor builds examples → Strategist designs attack plans → Obstructor stress-tests → Research Director prioritizes and assigns next actions.
Cross-cutting writing tools that operate on any document register — blog post, tutorial, lecture note, tech report, empirical paper, theoretical paper, Nature letter, policy essay. Designed to be invoked directly by an author and also called by other agents in the repo (proof-tutor, scientific-narrative-architect, 07-paper-structure-architect) so the discipline has a single canonical home.
Audits a draft against a calibrated narrative-clarity discipline. The discipline factors into universal rules (motivation precedes technique, concrete grounding before generality, no padding, pre-empt confusion at known stuck points, honest uncertainty, formalism after fluency, and expository weight proportional to difficulty) that apply at every register, and register-conditional rules that toggle by venue (personal voice, story-of-discovery proofs, physical metaphors, inline "where readers get stuck" warnings, plain acknowledgment of difficulty). The auditor takes a register parameter — blog | tutorial | lecture-note | tech-report | empirical-paper | theoretical-paper | nature-letter | policy-essay — and applies only the appropriate subset, surfacing a Deliberately not enforced section so the author can see which rules were suppressed by venue calibration rather than overlooked. This is the safeguard against the natural failure mode of "Feynman style": importing blog-style intuition and physical metaphors into a NeurIPS or Nature submission.
Rule 7 (expository weight proportional to difficulty) is the counterweight to over-polishing. Readers use expository weight to decide where to slow down: in human-written work the parts the author found hard retain a natural friction, and that friction is information. Uniformly smooth prose destroys it — a proof in which the load-bearing step and the change of variables read as equally easy leaves the reader nowhere to look. This is the characteristic signature of machine-polished exposition, which dwells on trivialities and passes briefly over the novel part, and the auditor flags it alongside two related patterns (missing high-level overview; the novel idea presented with no anchor to prior work at the point where it lands). Rule 7 is in deliberate tension with Rule 3 (no padding): cut padding everywhere, then verify that what survives is thickest at the hard parts. Minimizing length uniformly satisfies Rule 3 while violating Rule 7 — and is the more damaging error, because the result looks clean. The auditor is correspondingly forbidden to recommend rewrites that flatten a difficulty gradient.
The auditor is consumed by:
proof-tutor(lecture-note register) — invoked generatively before draftinglecture_notes.texand as an audit pass on each chapter.scientific-narrative-architect(register matched to itsAUDIENCEparameter) — invoked at the end ofDraft,Restructure,Adapt,Review, andQualityControlmodes.07-paper-structure-architect(paper register) — invoked per section after structural validation, to catch clarity issues that structure alone cannot.
Direct invocation:
# Audit a blog post draft
Use the narrative-clarity-auditor agent on draft.md with register: blog
# Audit a NeurIPS introduction — neutral tone, sparse metaphors
Use the narrative-clarity-auditor agent on intro.tex with register: empirical-paper
# Audit a theoretical paper section, allowing physical metaphors because the paper is itself about physical systems
Use the narrative-clarity-auditor agent on section3.tex with register: theoretical-paper, overrides: { metaphor_budget: moderate }
# Generative checklist (no draft) — produces clarity_checklist.md as a writing target for a lecture note
Use the narrative-clarity-auditor agent with register: lecture-note
The auditor emits clarity_audit.md with a calibration block, per-rule verdicts, anti-pattern findings, recommended minimal rewrites, and the deliberately-not-enforced list. Generative invocation emits clarity_checklist.md.
When the discipline changes, it changes here. Other agents reference; they do not duplicate.
Audits any agent output, draft, audit document, handoff record, or end-of-turn summary for the systemic positivity bias of LLM agents: language stronger than the evidence supports ("we show" when the evidence is consistent with X under conditions Y); coverage inflation ("Done", "all stages completed cleanly" without enumeration); marketing adjectives asserted rather than earned ("comprehensive", "robust", "novel"); and verdicts that have not been adversarially stress-tested. Three audit passes plus a devil's-advocate pass:
- Language calibration — does each claim's verb match the evidence ladder (proof / strong empirical / moderate empirical / weak / none)?
- Coverage calibration — are scope claims (Done, complete, all, every, fully, comprehensive) enumerated rather than asserted?
- Negative-result surfacing — are failed experiments, ablations that hurt, warnings encountered, and counter-evidence first-class outputs rather than glossed?
- Devil's advocate — for each load-bearing claim, what is the strongest plausible counter-argument? The author resolves; the auditor surfaces.
Critical design constraint: the auditor flags both overclaim and underclaim. Forced hedging on proven results is also a violation — the discipline is match language to evidence, not "always hedge". Strictness is set by an audit_target parameter (paper | audit_document | agent_handoff | status_report | blog | informal) so that paper claims are checked harder than internal status reports, but coverage enumeration is required at every target because "Done" without scope is the most common agent overclaim pattern.
The auditor is consumed by:
06-argument-architect— invoked after the claim-evidence matrix is built, withaudit_target: paper, before phase 06 declares done. Devil's-advocate alternatives must be addressed in the document, not merely acknowledged.08-research-revision-validator— invoked alongside its own linguistic-precision pass; the two complement (08 audits vagueness, this audits overclaim).proof-dissection-orchestrator,research-shaping-orchestrator— invoked ondissection_handoff.md/shaping_handoff.mdwithaudit_target: agent_handoffbefore reporting done. Catches "all stages completed cleanly" overclaim.
Direct invocation:
# Audit a paper draft (strictest)
Use the epistemic-calibration-auditor agent on draft.tex with audit_target: paper
# Audit an end-of-turn agent summary
Use the epistemic-calibration-auditor agent on summary.md with audit_target: status_report
# Devil's advocate pass on an audit document
Use the epistemic-calibration-auditor agent on prior_audit.md with audit_target: audit_document, evidence_sources: [experiment_logs.md, theorems.tex]
The capability-claim reporting schema. Any assertion about what an automated system can do — "the agent formalized the theorem", "closed in N cycles", "solved autonomously", "our pipeline discovers X" — triggers a dedicated schema. These are the least-well-calibrated claims in current technical writing for a structural rather than dishonest reason: the publicly available evidence is dominated by reporting bias and by results not gathered under controlled conditions, with costs and failed attempts undisclosed. A capability claim reported without its denominator is not a weak result, it is an uninterpretable one. The schema requires seven fields near the claim — denominator (attempts, not only successes), success rate with criterion, supervision level (prompt authorship, steering, selection among outputs, repair), cost per success, exact model and harness version, who verified it and independently of what, and whether conditions were controlled or observational. Missing denominator or supervision downgrades the claim to its actual scope rather than merely hedging it (hedging over a missing denominator is worse than the bare claim, because it reads as calibration while conveying nothing). The schema applies symmetrically to negative capability claims, and binds claims about your own agent pipeline as strictly as claims about a commercial model. A companion anti-pattern, metric-as-target drift, flags proxies asserted as goals — benchmark score for capability, rubric score for quality, coverage for correctness — since under heavy optimization the two come apart and a document that never names the underlying goal cannot detect that it has.
The auditor emits calibration_audit.md with the strictness profile, per-rule verdicts (overclaim/underclaim direction named), the capability-claim field audit, anti-pattern findings, the devil's-advocate alternatives with plausibility ratings, and minimal recommended rewrites.
The two writing auditors compose: narrative-clarity-auditor checks how the prose reads at the venue's register; epistemic-calibration-auditor checks what the prose claims relative to evidence. Both can run on the same draft, in either order.
Audits any document or repository for end-to-end provenance: every data file, script, figure, table, numerical claim in prose, and experimental result must trace back to a documented origin. The discipline is evidence-driven — no number, plot, or quoted result enters a document without a chain back to its raw input. Six universal rules: data files have provenance metadata (source, date, version, license, schema); scripts declare inputs and outputs; figures and tables have a producer trail (which script, which data, which version); numerical claims in prose are sourced (table / figure / citation / script output / stated experimental setup); experimental results have replication metadata (setup, hyperparameters, seeds, hardware, variability); transformations are documented step-by-step.
Companion to citation-provenance-auditor: that agent audits bibliographic provenance per citation; this one audits data and computational provenance. Together they cover the full evidence chain a reader needs to verify a claim.
Anti-pattern catalog covers: magic constants in scripts (threshold = 0.05 with no comment), headerless data files, figures without producer scripts, "data from [partner]" without specifics, hard-coded local paths signalling un-portable provenance, silent re-runs without seeds documented, and unsourced statistics in prose.
The auditor is consumed by:
04-research-data-architect— primary upstream user; data-design output gets audited before downstream phases.05-research-analysis-interpreter— invoked after results to verify replication metadata and chain integrity.06-argument-architect— every numerical claim in the claim-evidence matrix must have an intact chain (claim → table/figure → script → data → source) before phase 06 declares done.08-research-revision-validator— invoked alongside epistemic-calibration before sign-off.09-research-validation-qa— chain-integrity directly answers the reproducibility question.scientific-narrative-architect— invoked when prose contains numerical claims, inReviewandQualityControlmodes.
Direct invocation:
# Audit a paper repo end-to-end
Use the evidence-provenance-auditor agent on /path/to/paper-repo with audit_target: paper_repo
# Audit only the data directory
Use the evidence-provenance-auditor agent on /path/to/repo/data with audit_target: data_artifacts
# Audit a blog post that quotes statistics
Use the evidence-provenance-auditor agent on draft.md with audit_target: blog_with_data
The auditor emits provenance_audit.md with an inventory of artifacts in scope, per-artifact provenance verdicts, chain-integrity walks, anti-pattern findings, and minimal recommended patches (a header to add, a preamble to write, a footnote to insert). It does not produce data, scripts, or prose; it traces and recommends.
This is not a new agent — it documents how the existing citation-provenance-auditor (detailed under Cross-Phase Tools) participates in the writing-auditor family. The auditor has gate semantics: no citation enters a document without a provenance record from it first. Severity-tiered to keep the gate from becoming a bottleneck:
- Tier-1 (load-bearing) — citations supporting Tier-1/Tier-2 claims, baselines, or canonical references. Strict gate before acceptance.
- Tier-2 (supporting) — contextual citations. Light gate (persistent identifier + metadata only); claim-mapping deferred to a batch pre-submission pass.
- Tier-3 (peripheral) — tangential references. Batch gate before submission only.
Suggesting agents (literature-expansion, 02-literature-discovery-mapper, 06-argument-architect, scientific-narrative-architect, arxiv-gap-scanner) treat the auditor as a gate, not a downstream check. Failed Tier-1 citations are replaced, demoted, or dropped — never silently retained. Each suggesting agent's Definition of Done now reflects this contract.
Audits how theorems and proofs are presented in a paper, lecture note, or technical document. The dominant failure mode of theoretical papers is "wall of theorems with proofs": pages of formal statements with no signposting, no separation of load-bearing from bookkeeping moves, no clear answer to what does this theorem do for the paper's argument. Reviewers cannot tell on a first pass what to scrutinize. The auditor inverts that failure mode by enforcing two reviewer-centric disciplines:
Part A — Theorem rhythm. Every theorem the paper invokes for its argument is surrounded by four elements in fixed order:
- Theorem statement — formal, with all assumptions named in the statement.
- Intuition — plain-language meaning, marked explicitly ("Informally,…").
- Operational interpretation — what the theorem does: how it gets used, what computational/algorithmic/argumentative consequence it produces.
- Consequence — what changes downstream in the paper's argument because this theorem holds.
The rhythm can take three compliant forms (inline / sectioned / pre-stated) but the four elements must all be present.
Part B — Modular proof architecture. Every non-trivial proof is structured for reviewer skimmability:
- Proof sketch in main text — names the proof technique, identifies the one or two load-bearing steps, references key lemmas by name, readable in 30 seconds.
- Key lemmas extracted and named — non-trivial intermediate results are named lemmas with their own rhythm (Part A).
- Full formal proof in appendix — with
\labels matching the sketch's named load-bearing steps for bidirectional cross-reference. - Significance tagging — each step in the sketch tagged
[load-bearing] | [technical] | [bookkeeping](via inline tags, macros, or consistent typographic convention) so reviewers see at a glance what to scrutinize vs. take on faith.
Anti-pattern catalog covers: theorems with no intuition, operational interpretation absent (the theorem floats free of the paper's argument), proofs running uninterrupted for two pages without named lemmas, "by a tedious but standard calculation" without elaboration, all steps presented as equally important, lemmas cited from prior work without their own intuition, inline anonymous claims doing real work, appendix proofs without labels matching the sketch, and significance tagging applied as decoration (every step labeled load-bearing, defeating the purpose).
Register calibration: required for theoretical-paper and empirical-paper; rhythm-only with delegated architecture for lecture-note (proof-tutor's story → formal pattern carries the architecture role); compact rhythm for nature-letter; encouraged for tech-report; refused for non-theorem-bearing registers.
The auditor is consumed by:
07-paper-structure-architect— invoked after section-level structural validation. Section structure and theorem-internal architecture are orthogonal and both required.scientific-narrative-architect— invoked when introducing or repositioning theorems; complements its existing Theorem-Empirical Alignment (Section X) which audits a different concern.06-argument-architect— every theorem in the claim-evidence matrix's evidence column must pass the rhythm audit, because the operational interpretation is the bridge between the theorem and the claim it supports.proof-tutor(lecture-note register) — Part A applies (rhythm required for every chapter); Part B is delegated to the tutor'sstory → formal → loose-endspattern.
Direct invocation:
# Audit a theoretical paper
Use the theorem-presentation-auditor agent on draft.tex with register: theoretical-paper
# Audit only the architecture of one chapter (lecture note delegates Part B)
Use the theorem-presentation-auditor agent on chapter3.tex with register: lecture-note, scope: T1
# Audit a Nature letter — compact rhythm, no architecture
Use the theorem-presentation-auditor agent on letter.tex with register: nature-letter
The auditor emits theorem_presentation_audit.md with theorem inventory, per-theorem rhythm verdicts (statement/intuition/operational/consequence/order/exemption), per-proof architecture verdicts (sketch/technique/load-bearing/lemmas/location/tagging), anti-pattern findings, and minimal recommended patches.
Audits how the work was produced, and drafts the disclosure statement it should carry. Third leg of the provenance triad: citation provenance audits where claims came from, evidence provenance audits where numbers came from, this audits where the work came from. Takes an audit_target — paper | paper_repo | formal_development | technical_report | blog | agent_pipeline_report — and optional process_evidence (session logs, commit history, Story of the Proof sections, lean-proof-chain-validator Phase 7.3 records); without evidence the run is marked unverified-ledger rather than silently asserting verification.
The core artifact is an assistance ledger: every component of the work assigned a level on a seven-rung ladder from A0 (none) through A3 (drafting from an author-specified outline), A4 (the tool originated content the author verified), A5 (author selected among candidate outputs) to A6 (author neither specified nor meaningfully checked it). The A3/A4 boundary is where understatement concentrates — "drafting assistance" over content the tool originated is the most common inaccurate disclosure — and A6 is an escalation rather than a level, because it is exactly the state in which a correct result enters the record with nobody able to explain it. The audit then compares the ledger against any existing disclosure (understated / overstated / unlocated), sweeps A3+ components for unattributed reuse of prior work (routed to citation-provenance-auditor, never adjudicated here), records verification independence per A4+ component, and checks four responsibility invariants: correctness and citations remain the authors' alone, authorship is human, and the register is factual rather than apologetic.
It has no view on how much assistance is appropriate — an A5-heavy ledger disclosed accurately is ACCURATE. It also refuses to infer levels from writing style: prose that "sounds AI-generated" is not evidence, and a wrong accusation is worse than a missing disclosure. Grounded in the Leiden Declaration (June 2026, IMU-endorsed) and Tao's ICM 2026 argument that covert use — not heavy use — is the outcome to avoid.
Direct invocation:
# Audit a manuscript before submission
Use the ai-contribution-disclosure-auditor agent on paper.tex with audit_target: paper, process_evidence: sessions/
# Audit a Lean development that passed Phase 7
Use the ai-contribution-disclosure-auditor agent on Formal/ with audit_target: formal_development
# Check whether an existing disclosure statement is accurate
Use the ai-contribution-disclosure-auditor agent on paper.tex with audit_target: paper — is "editing assistance" supportable?
The auditor emits disclosure_audit.md with the assistance ledger, disclosure mismatches, unattributed-reuse candidates, verification-independence records, responsibility-invariant checks, a ready-to-paste disclosure statement, and an ACCURATE / UNDERSTATED / UNLOCATED / ABSENT / UNVERIFIED-LEDGER verdict.
The six writing auditors compose. They cover orthogonal concerns:
| Auditor | Audits |
|---|---|
narrative-clarity-auditor |
How the prose reads at the venue's register |
epistemic-calibration-auditor |
What the prose claims relative to evidence (overclaim + devil's advocate + capability claims) |
evidence-provenance-auditor |
That the evidence chain exists (data → script → figure → claim) |
citation-provenance-auditor |
That cited works are real, canonical, and support the cited claim |
theorem-presentation-auditor |
That every theorem has rhythm and every proof has reviewer-skimmable architecture |
ai-contribution-disclosure-auditor |
How the work was produced (assistance ledger → disclosure accuracy → unattributed reuse) |
A paper that passes all six is reproducible, defensible, honest about what it claims, honest about how it was made, and structured for the reviewer to triangulate at a glance.
Which agents invoke which writing auditors, and at what gate. Cell content names the trigger.
| Caller | narrative-clarity | epistemic-calibration | evidence-provenance | citation-provenance | theorem-presentation | ai-contribution-disclosure |
|---|---|---|---|---|---|---|
06-argument-architect |
— | DoD: claim-evidence matrix | DoD: numerical claims | DoD: matrix evidence column (Tier-1 strict gate) | DoD: theorems in evidence column | — |
07-paper-structure-architect |
per-section clarity audit | — | — | — | per-section theorem audit | — |
08-research-revision-validator |
— | paired with linguistic-precision pass | — | (via citation gate, upstream) | — | — |
09-research-validation-qa |
— | reproducibility-grade audit | reproducibility-grade audit | — | — | ledger as reproducibility finding |
10-scholarly-submission-strategist |
— | — | — | — | — | DoD: disclosure statement in digestion_plan.md |
scientific-narrative-architect |
end of Draft/Restructure/Adapt; XV.5 in Review/QC | (via narrative-clarity) | numerical claims in prose | new-bibkey gate at suggestion | introduce/reposition theorems | — |
proof-tutor (lecture-note) |
self-check before emitting .tex |
— | — | — | rhythm required (Part A); architecture delegated | — |
proof-dissection-orchestrator |
— | handoff record audit | — | — | — | — |
research-shaping-orchestrator |
— | handoff record audit | — | — | — | — |
literature-expansion |
— | — | — | bundle entries (Tier-1 strict gate) | — | — |
02-literature-discovery-mapper |
— | — | — | necessity-supporting citations (Tier-1) | — | — |
arxiv-gap-scanner |
— | — | — | critical-tier surfaced works (Tier-1) | — | — |
ai-paper-reviewer |
(optional, ground individual critiques) | (optional, ground individual critiques) | — | — | — | — |
lean-proof-chain-validator |
— | — | — | — | — | Phase 7.3 record feeds the ledger |
venue-archetype-distiller |
— | scorecard Goodhart check (optional) | — | (citation gate on cited exemplars) | — | — |
The matrix encodes the design principle: auditors are canonical, callers reference, and gates fire at the moment overclaim or missing provenance does the most damage. New agents that suggest citations or claim coverage should add themselves to this matrix.
Validates Lean proof chains for research-grade correctness across seven phases: scope locking (freezing Lean/mathlib versions), logical soundness (zero sorry/admit/warnings), dependency closure (frontier YAML validation and axiom boundary checks), epistemic validation (novelty integrity, claim-proof alignment, quantifier discipline), infrastructure assessment (mathlib compatibility, conceptual compression), robustness (proof stability, rebuild/replay, boundary cases), and negative-result capture. Issues PASS/CONDITIONAL/FAIL verdicts with specific file/line references.
Phase 7 — the explicability gate. A correct, closed, robust proof chain that nobody can explain is a liability, and machine-checked proof makes that state reachable in a way it previously was not. The final phase requires, for the root theorem and every @novelty.level ≥ 3 theorem, a natural-language account that states the proof idea (mechanism, not tactic sequence), keys each step to named entities in the formal chain, names the one or two steps carrying the difficulty, and says why the obvious approach fails. A paraphrase of the tactic script does not satisfy it. Absent such an account the verdict is FAIL regardless of Phases 1–6 — a green build with zero sorries and no explanation invites downstream reliance nobody can audit. The phase also tags each step load-bearing | technical | bookkeeping (the same vocabulary as theorem-presentation-auditor, so tags transport into any paper written from the development) and checks that expository weight tracks the tags, and records process provenance — agent/human split, harness version, attempts to success, cost — which feeds ai-contribution-disclosure-auditor at writeup.
Performs breadth-first proof dependency analysis on Lean 4 formalizations. Constructs complete dependency DAGs by recursively expanding until every leaf is classified as mathlib, assumed, novel, or infrastructure. Assigns novelty levels (0-5) along five axes (conceptual, theorem, formalization, structural, methodological). Documents axiom boundaries with precise Lean statements and source citations. Generates frontier YAML files and provenance markdown with dependency summaries. Emits design_flags (redundant renames, def-not-abbrev, trivial aliases, duplicate objects) that feed the library-design auditor.
Every provenance file also carries a Story of the Proof section: the route taken and why this proof, the routes abandoned with the reason each failed, where the difficulty lived, what the formalization revealed that the informal argument had hidden, and the agent/human provenance of the work. The DAG records what worked and is structurally silent on what did not; this section is the only place the abandoned routes survive, and it is the raw material for the exposition that has to exist before anyone else can digest the result. Capture it while the development is fresh — it is not reliably reconstructible afterwards.
Audits a compiled, sorry-free Lean development for reusability rather than correctness — the orthogonal question of whether the result is a library contribution a future formalizer can build on without transport pain. Reviews the four surfaces where autoformalization reliably fails: definitions (redundant renames, def-where-abbrev-transports, hyper-specific Equivs that should be inlined ofBijective, use-case naming, duplicates), theorem-statement generality (hypotheses stronger than the proof uses, conclusions special-cased for convenience), API surface (downstream code unfolding definitions instead of routing through lemmas; ad-hoc lemma piles with no principled interface), and file/namespace organization (bottom-up import graph, descriptive names). Enforces the proof-cost rule (maxHeartbeats ≤ 200000 — decompose into named sublemmas rather than inflating the budget) and flags escape-hatch language. Separates findings into an agent-actionable completion-predicate worklist and design decisions requiring human judgment, then issues a DESIGN-READY / NEEDS-REWORK / NEEDS-DESIGN-DECISION verdict. Premise: kernel acceptance is an incomplete evaluation target — closing sorries is not the hard part; choosing what objects should exist is.
Where it sits. This is the canonicalization stage of the pipeline. mathlib is the canonicalization infrastructure of formalized mathematics, and asking whether a development is something a future formalizer would build on is the digestion question — the slowest stage, the least automatable, and the most valuable. A NEEDS-REWORK verdict is not pedantry about style; it is the difference between a result that enters the shared corpus and one that sits in a repository nobody extends. A third cross-cutting rule records adoption evidence — independent downstream imports, in-project reuse across proof boundaries, single-call-site objects, upstream mathlib PR status — because reusability is a claim about the future that the author is the party least able to certify. Where no adoption evidence exists, DESIGN-READY is labelled as a prediction rather than reported as an established property.
The sync script creates symlinks from ~/.claude/agents/ to the repo, keeping everything in sync:
./scripts/sync-agents.shThe script:
- Creates symlinks for all
.mdfiles underagents/ - Warns (does not overwrite) if a regular file already exists at the target
- Removes stale symlinks from previous syncs
- Is idempotent — safe to run repeatedly
# Copy all agents
find agents -name "*.md" -exec cp {} ~/.claude/agents/ \;The math brainstorming agents support persistent agent memory at ~/.claude/agent-memory/{agent-name}/. This allows agents to accumulate knowledge across sessions — recording which patterns worked, which approaches failed, and what structural insights were discovered.
Memory setup is user-local and not tracked in this repo. Each agent's spec references its memory directory; the memory infrastructure is created automatically on first use.
Each phase has explicit "Definition of Done" criteria. A phase is complete when:
- All gate checks pass
- A hostile reviewer cannot identify a phase-specific fatal flaw
- A benevolent reviewer can articulate why the phase adds value
- Artifacts are documented and reproducible
Common rejection signals by phase:
| Phase | Hostile Reviewer Attacks |
|---|---|
| 01 | "Why should anyone care?" / "This is a toy problem" |
| 02 | "They missed X which already does this" / "Incremental over Y" |
| 03 | "This evaluation does not test the claim" |
| 04 | "Dataset is too small" / "Benchmark favors their method" |
| 05 | "This could be noise" / "No error bars" |
| 06 | "They did not actually show this" / "Correlation ≠ causation" |
| 07 | "I don't understand what they did" |
| 08 | "Sloppiness indicates deeper problems" |
| 09 | "I could not reproduce this" |
| 10 | "This is merely incremental" / "Who will cite this?" |
MIT