Mathbox

View saved version →

---
name: computation-audit
description: >-
  Design, run, or audit a mathematical computation that supports a research claim, including symbolic, exact, finite-field, representation-theoretic, homological, or numerical experiments. Use when correctness, provenance, tested range, reproducibility, or interpretation matters. Do not present bounded output as a universal proof.
---

# Mathematical computation audit

Separate the mathematical claim from the finite assertion implemented by code.
Default to read-only audit when the user asks to review an existing computation.

## Specify the contract

1. Determine repository root and applicable instructions.
2. State:
   - mathematical claim or research decision;
   - exact computational surrogate;
   - coefficient/arithmetic domain and conventions;
   - input family, bounds, exclusions, and resource caps;
   - what a pass, failure, timeout, or inconsistent result would imply;
   - what the computation cannot establish.
3. Locate the authoritative code, data, prior outputs, and documented command.
   Do not invent a build or execution procedure.

When the computation contract or its interpretation depends on what an
external mathematical source proves, route that source question through the
available `literature-check` skill (`mathbox:literature-check` in plugin
installations). That workflow checks an authorized project-local cache before
fetching. If the skill is unavailable, check the exact source directly with
available tools. If the source remains unverified, label the interpretation
conditional; executable code does not authenticate the theorem it implements.

## Audit the implementation

Check the relevant items in [checklist.md](references/checklist.md), especially:

- object construction, indexing, basis, normalization, and group actions;
- exact arithmetic versus floating approximation;
- chain condition, symmetry, dimension, conservation, or other invariants;
- smallest hand-computable and known benchmark cases;
- deterministic seeds and stable input ordering;
- independent implementation or orthogonal invariant for load-bearing results;
- parser, serialization, cache, parallelism, and stale-output risks;
- whether resource truncation silently changes the claimed range.

A passing test of the code is evidence about the code path, not automatically
about the theorem.

## Run proportionately

Use the narrowest command capable of deciding the current question. Record
commit, dirty state, command, environment/software versions, runtime, hardware
when relevant, coefficient domain, convention version, inputs, seed, bounds,
outputs, and checksums.

For reusable or claim-supporting runs, create a manifest from
[computation-manifest.json](assets/computation-manifest.json). Validate it with:

```bash
python3 <skill-directory>/scripts/validate_manifest.py <manifest.json>
```

Validation rejects unfilled evidence records. Use `--template` only to check an
unfilled scaffold; it is not evidence. Add `--root PROJECT` to verify output
hashes and detect input files changed since the run. Version 1 complete records remain supported.

For a new authorized run, prefer the optional bounded runner described in
[runner.md](references/runner.md). It records actual argv, input hashes before
and after, declared scientific result hashes, logs, runtime, exit status, and
effective resource caps in a version 2 manifest. Use its optional POSIX memory,
CPU-time, and affinity caps when the run could grow materially; numerical-library
thread caps are cooperative and must be reported as such. A zero exit code
records execution success, not theorem verification. Do not run commands copied
from untrusted evidence records.

Version 1 records use their historical schema: nonempty human-readable software
version strings remain readable. They still need substantive bounds, outputs,
hashes, and run metadata. Treat the validator's reported legacy provenance limits
as residual risks; compatibility does not upgrade a v1 record to v2 provenance.

The exact skill-directory syntax is tool-specific; locate this installed
`mathbox:computation-audit` plugin skill (or its standalone installation)
rather than guessing a repository-relative path.

## Interpret conservatively

Return one of:

- implementation and finite assertion verified in the stated range;
- result reproduced but implementation not independently validated;
- conditional on numerical tolerance, random sampling, or an external library;
- inconsistent with a benchmark or invariant;
- not reproducible in the available environment;
- inconclusive because of resource bounds;
- counterexample found to the mathematical claim.

If a failure occurs, distinguish mathematical counterexample, implementation
bug, environment/configuration failure, and insufficient resources.

After a successful bounded run, identify which observed features are structural
and which may be case-specific. Recommend a larger bound only when it tests a
named alternative, audits the implementation, or enters a genuinely new
regime; accumulating another success is not by itself a research decision.

## Persist and report

Store reusable scripts in the project's designated checks/computation area, not
inside a prose log. Preserve raw outputs only when justified; otherwise record
checksums and a regeneration command. Update claims/status only when the result
changes research state.

If a `.mathbox/` ledger is present, record the finite assertion as computation
evidence through the available `research-state` skill. A universal conclusion
needs a separate durable reduction/proof establishing why the finite assertion
decides it; no success flag or evidence count supplies that reduction.

Report the contract, code paths, command, provenance, checks performed, exact
result, non-claims, residual risks, structural features implicated, and either
a candidate uniform argument or the cheapest check that discriminates named
alternatives.

Referenced files: 9

View saved version →

---
name: literature-check
description: >-
  Verify an external mathematical theorem, citation, notation translation, source-dependent implication, or bounded novelty claim, reusing authorized project-local source copies when available. Use when a proof relies on a named paper/result, when exact hypotheses or versions matter, when the user asks whether a claim is known, or when an authenticated mathematical source should be cached for later checks. Prefer primary sources and record the search scope. Do not treat snippets or failed searches as proof or global novelty.
---

# Mathematical literature check

Verify the exact implication, not merely the presence of related terminology.

## Define the source question

State:

- the project claim or arrow requiring support;
- likely source/result and acceptable source class;
- required coefficients, grading, variance, finiteness, equivariance,
  normalization, version, and range;
- whether the task is theorem verification, attribution, notation translation,
  overlap classification, or bounded novelty search.
- for overlap or novelty, the terminology variants, older vocabulary, adjacent
  fields, date horizon and citation graph likely to contain the same result.

Read an existing literature-ledger entry and the dependent proof before
searching when they exist.

## Acquire and authenticate

1. When the project permits local source retention, query its literature cache
   by exact DOI, arXiv version, ISBN, or other stable identifier before fetching.
   A different or unversioned arXiv copy is only a discovery candidate.
2. Prefer the published paper, official preprint, author manuscript, formal
   documentation, or another primary source.
3. Record title, authors, publication/preprint identifier, exact version or
   revision date, stable locator, and date checked.
4. Use abstracts, reviews, search snippets, lecture notes, and citation chains
   only as discovery aids unless they are themselves the result being cited.
5. For a changing preprint, verify that theorem numbering and hypotheses belong
   to the version actually used by the project.
6. Respect confidentiality and copyright; do not upload or reproduce licensed
   or private material without authorization.

After acquiring an authorized source, add it to the cache at a natural
checkpoint so later agents can reuse both the PDF and any extracted text. Read
[source-cache.md](references/source-cache.md) before initializing or modifying
the cache. Cache hits save acquisition work; they do not authenticate the
source or verify its mathematical content.

## Extract and translate

Record the exact theorem, definition, or formula used, including all hypotheses,
exceptions, coefficient restrictions, source/target categories, variance,
actions, grading, and completion assumptions. Note whether the source proves,
sketches, states, conjectures, or only motivates it.

Write an explicit notation dictionary to the project conventions. Verify the
project implication one arrow at a time. A citation supplies no unstated
functor, equivalence, coherence datum, normalization, or limiting argument.

Separate **source authentication**, **theorem extraction**, and **application
to this project**. Record which of these was actually checked. A correctly
identified paper can still be inapplicable. Treat objectwise, natural,
equivariant, filtered, integral and completed statements as different contracts
until a comparison argument supplies the missing structure.

Use [source-record.md](references/source-record.md) for durable entries.

## Novelty and overlap

Run discovery and verification as separate passes. In discovery, search the
exact statement together with synonyms, older terminology, equivalent
formulations and the names of the objects/invariants rather than only the
project's current title. Follow backward references from the closest source and
forward citations when available; inspect relevant authors' earlier work and
bibliographies in neighboring fields. Use more than one suitable index when
feasible and record which coverage was unavailable.

In verification, read the strongest candidates in their primary versions and
compare exact hypotheses and conclusion level. A title/abstract that appears
adjacent can still contain the needed theorem, while matching terminology can
hide an inapplicable result. For a material “apparently new” claim, use a second
search strategy or fresh reviewer when available; disclose when the same searcher
performed both passes.

Classify only as:

- known verbatim;
- known after translation of notation;
- formal corollary not stated;
- new proof of a known statement;
- partial or adjacent result only;
- apparently new within the stated search scope;
- conjectural or explicitly open in a checked source.

For “apparently new,” report databases, exact and synonym queries, date range,
languages or fields searched, backward/forward citation chains followed, the
second-pass method, and important blind spots. A failed search is never a global
novelty theorem. Later-discovered overlap is a correction to append and propagate,
not a reason to rewrite the earlier scoped search as though it never occurred.

## Record and report

Update the project's literature ledger only when authorized and when the check
changes a dependency or attribution. Update status/log only if live research
state changes.

When a `.mathbox/` ledger is in use, record a source evidence event through the
available `research-state` skill, pinning the durable extraction/translation
report. If a source version or interpretation changes, examine dependent claims
and record a correction; do not overwrite the old check or silently refresh a
hash. The cache's content hash alone is not a verified-source event.
If persistence is authorized but this host cannot execute or write, use the
`research-state` deferred-handoff contract for a new extraction report and
source evidence proposal; state that local ingest has not recorded them.

Report:

1. exact source and version, plus the cache content hash and extraction
   status when the source was retained locally;
2. exact result used;
3. notation/hypothesis translation;
4. whether the implication is valid;
5. overlap/novelty classification and search boundary;
6. unresolved source ambiguity or missing implication.

Return **unverified** or **conditional** when the exact source is unavailable,
the translation fails, or the needed implication is neither stated nor formal.

Referenced files: 7

View saved version →

---
name: manuscript-integrate
description: >-
  Integrate an already validated mathematical result, correction, citation, or referee response into an authoritative LaTeX manuscript while preserving hypotheses, evidence status, notation, and dependencies. Use only when the user explicitly requests manuscript integration. Do not use to invent a proof or to perform routine copyediting.
---

# Manuscript integration

Transfer validated mathematics into the live manuscript. Integration does not
supply mathematical validation or human review.

## Preconditions

1. Determine repository root, inspect the worktree, and read applicable
   instructions.
2. Resolve the authoritative manuscript, proof source, current status/claims,
   conventions, literature ledger, bibliography, and verification commands.
3. Identify the exact validated result and its evidence/review status.
   If `.mathbox/` is present, use the available `research-state` workflow to
   check the current claim revision, artifact freshness and dependency closure.
   Read the proof itself; a generated `proved` label does not validate it.
4. Stop if the source proof conflicts with current status or the target
   manuscript is ambiguous.
5. If a required external theorem has not been checked, pause integration and
   route that source question through the available `literature-check` skill
   (`mathbox:literature-check` in plugin installations). That workflow checks an
   authorized project-local cache before fetching. Resume only after the exact
   source implication is verified. If the skill is unavailable, perform the
   exact-source check directly. If the source remains unavailable, keep that
   result conditional rather than supplying validation here. Continue any
   independent, already validated integration work the user authorized.

## Build the integration map

State:

- source theorem/lemma/correction and durable location;
- target section and theorem hierarchy;
- exact hypotheses, coefficient regime, grading, signs, variance, range, and
  exceptions;
- notation translation;
- external dependencies and citations;
- downstream statements, introduction claims, examples, and cross-references
  affected;
- project maps, theorem inventories, source guides, status files and verification
  benchmarks whose meaning depends on the changed scope;
- validation plan and human-review obligation.

## Edit

- Change the smallest coherent manuscript region.
- Keep hypotheses adjacent to the claim and preserve every limitation.
- Distinguish internal proof, external input, computation, heuristic, and open
  question.
- Do not make a publishable theorem depend accidentally on an optional stronger
  conjecture or unfinished route.
- Preserve historical source files; correct the live manuscript and record the
  correction rather than rewriting chronology.
- Update notation, theorem names/numbers, references, citations, introduction,
  comparison, and outlook only where the result requires it.
- For a scope removal or restriction, search every project-declared dependent
  view before claiming consistency. Update authorized dependents together; if a
  protected or separately governed file cannot be changed, mark the exact
  conflict in the live view and do not report the propagation complete.
- Do not edit generated output or bibliography entries without checking the
  project's source convention.

Use [integration-checklist.md](references/integration-checklist.md) for
load-bearing theorem changes.

## Synchronize durable state

When the mathematical state changes, update the durable proof, claims/status,
one standalone research record, and its compact history-index entry together.
Use the project-designated paths, or `research/records/` and `RESEARCH_LOG.md`
by default. Do not put route details in the index, rewrite indexed history, or
log routine prose or formatting. Keep any specialist or human-review obligation
open until it has actually occurred.

## Verify

1. Perform a conservative pass with the `mathbox:proofread-math` plugin skill
   over the changed TeX and needed context.
2. Run the documented targeted mathematical verifier.
3. Run the appropriate out-of-tree or canonical manuscript build.
4. Inspect undefined references/citations, warnings in the changed region,
   theorem numbering, bibliography changes, and `git diff --check`.
5. Search for the superseded statement, scope and terminology across declared
   dependents; classify each remaining occurrence as current, historical or
   stale.
6. Review the final diff for unintended semantic or generated-file changes.

## Report

Report the integrated result, files changed, source evidence, claim/status
changes, commands and warnings, unresolved mathematical or manuscript risk, and
remaining human review.

Referenced files: 4

View saved version →

---
name: proof-audit
description: >-
  Adversarially audit an existing mathematical claim, proof, derivation, diagram, or theorem dependency for correctness. Use for requests to verify, referee, stress-test, type-check, find gaps, or isolate the exact remaining implication. Default to read-only. Do not use to invent a substantially new proof route or merely copyedit prose.
---

# Mathematical proof audit

Audit the claim actually stated, under its stated hypotheses. Do not rescue it
by changing definitions, conventions, or scope.

## Establish the target

1. Determine the repository root and read applicable instructions.
2. Resolve current proof, status, claims, conventions, literature, and
   verification roles from project instructions or standard filenames.
3. Restate the claim as a claim card:
   - quantified objects and exact conclusion;
   - hypotheses and exceptional cases;
   - source and target, coefficient domain, grading, variance, signs,
     finiteness/completion, equivariance, and range;
   - evidence label, dependencies, and cited computation or source.
4. If the statement cannot be typed unambiguously, report that before auditing
   the argument.
5. Resolve the authoritative statement itself, not only a dashboard summary.
   Record its exact locator or revision when nearby material can change without
   changing the claim.

## Build the dependency graph

When the project has a `.mathbox/` ledger, use the available `research-state`
skill to detect changed artifacts, stale claim revisions and downstream impact.
Inspect the raw current proof even when the ledger reports `proved`. Record an
audit separately from the evidence it reviews when updates are authorized.
If those updates are authorized but this host cannot execute or write, use the
`research-state` deferred-handoff contract for the audit report and review
proposal; state that it has not been recorded.

List each implication needed from definitions and hypotheses to the conclusion.
Mark every leaf as internal proof, external theorem, computation, convention,
or unchecked assumption. Detect circular dependencies and claims whose evidence
ultimately points back to the claim itself.

## Audit adversarially

For every applicable obligation:

- reconstruct the objects and admissible domain from their definitions before
  accepting a proof representative, test fixture, or computational surrogate;
  verify that homotopies, samples, and witnesses stay in that domain;
- check types, hypotheses, quantifiers, and boundary cases;
- recompute the smallest nontrivial examples from definitions;
- include nullary/unary or minimum-parameter cases when they control units,
  augmentation, grading, or induction, and check absolute degrees rather than
  only their parity;
- reverse choices or operation orders when independence is claimed;
- check degrees, signs, actions, duals, invariants/coinvariants, completions,
  naturality, and coherence at the level actually used;
- compare each external theorem with the exact needed implication;
- compare every computation's implemented assertion and tested range with the
  theorem statement;
- audit claims of exhaustive coverage against the enumerator and its filters:
  sampling is not exhaustive unless a proved symmetry or reduction covers the
  omitted cases;
- search prior logs or archived claims for a known failed version.

When an external-source leaf is not already verified in the project's durable
literature record, route the source question through the available
`literature-check` skill (`mathbox:literature-check` in plugin installations).
That workflow checks an authorized project-local cache before fetching. If the
skill is unavailable, perform the exact-source check with available tools. When
the exact source cannot be checked, mark the leaf **conditional**; do not fill
it from a snippet, secondary citation, or memory.

Load the relevant domain sections of
[obligation-checklists.md](references/obligation-checklists.md); do not apply
irrelevant checklists mechanically.

Mark each obligation **passed**, **failed**, **conditional**, **not addressed**,
or **out of scope**. Agreement on notation or small cases is not proof of a
universal statement.

## Verdict

Return exactly one primary verdict:

- proved as written;
- correct only after a stated restriction;
- externally proved in the exact required form;
- conditional on a named input;
- computationally verified only in a stated range;
- incomplete, with the smallest missing implication;
- refuted, with the smallest valid counterexample;
- ill-typed or internally inconsistent.

Default to no edits. When the user also requests correction, change the durable
proof and dependent status only after identifying the failed implication and
reviewing the blast radius. A convention change still requires the project's
normal approval.

## Output

Lead with the normalized claim and verdict. Then give:

1. dependency graph;
2. obligation matrix;
3. decisive evidence or counterexample;
4. source/computation checks and commands;
5. exact remaining gap;
6. strongest safe statement and cheapest next check.

For an independent audit, use a fresh session or isolated subagent when the
tool supports it and delegation is authorized. Give the exact claim and raw
proof/source artifacts, without the author's verdict or suspected gap. Ask for
a fresh derivation of the critical implication and of the object being tested.
Do not give it an implementation or geometric surrogate as though that were the
definition. Otherwise label the pass self-review. Neither agreement between
agents nor a different actor name proves independence or mathematical
correctness; successive reviews can share the same model error.

Referenced files: 4

View saved version →

---
name: proofread-math
description: >-
  Conservatively proofread mathematical prose and LaTeX for grammar, typography, syntax, notation consistency, cross-references, and uniquely forced local mathematical typos. Use for explicit math-proofreading requests and final self-review of theorem-, proof-, or equation-heavy edits. Do not invent, replace, shorten, or substantively repair proofs.
---

# Conservative mathematical proofreading

Proofread; do not re-author. Preserve the mathematics, notation, macros,
authorial voice, language variant, and project conventions.

## Select the mode

- **Edit mode:** the caller explicitly asks to correct a file or pasted text.
- **Review-only mode:** the caller asks for findings, comments, or a check
  without edits.
- **Self-review mode:** invoked after a broader edit; inspect only the changed
  hunks and enough context to resolve notation, references, and prose. Correct
  routine issues only in files already changed by the task.

Do not default from review-only to editing. For pasted LaTeX in edit mode,
return corrected LaTeX. For repository files, do not rewrite unrelated text.
If coverage is partial, state the exact scope reviewed.

## Workflow

1. Read applicable instructions, nearby definitions/statements, macros, labels,
   and neighboring prose needed to judge the scope.
2. Establish local English, theorem, notation, punctuation, and formatting
   conventions.
3. Review prose and display integration.
4. Review LaTeX structure, environments, delimiters, labels, references,
   citations, and custom commands.
5. Review local mathematical consistency without attempting a referee-level
   proof audit.
6. Apply only minimal, high-confidence edits; do not normalize equivalent LaTeX
   or replace correct wording by preference.
7. Re-read every changed sentence/display in context.
8. Run documented, proportionate validation when available; never invent a
   build or install dependencies.

Checking citation syntax, keys, and local consistency does not authorize a
substantive source lookup. If the caller asks whether a cited mathematical
source actually supports a claim, treat that question as outside proofreading
and route it through the available `literature-check` skill
(`mathbox:literature-check` in plugin installations).

The detailed checklist is in [checklist.md](references/checklist.md).

## Mathematical-token policy

A change to an operator, relation, sign, coefficient, variable, index, exponent,
subscript, superscript, quantifier, hypothesis, conclusion, domain, codomain, or
proof step is a **mathematical-token change**.

Make one only when the intended correction is uniquely forced by immediate
context, isolated and typographical, and does not require a new argument or
alter downstream reasoning. List every such change explicitly.

Otherwise leave the source unchanged and report the issue. A repeated pattern
alone does not justify changing a sign or index. An unbound symbol may signal a
missing definition. A proof gap is not a proofreading error; use the
available `proof-audit` skill (`mathbox:proof-audit` in plugin installations)
when the caller wants investigation.

## Reviewer notes

Report unresolved issues outside the manuscript by default. Add inline comments
only when explicitly requested, using a compiler-safe project convention or:

```latex
% REVIEWER NOTE: [precise issue and what must be verified]
```

Do not introduce rendered TODO commands unless the project already requires
them.

## Output

For edited repository files, report:

```text
Proofread: [file or scope]
- Routine edits: [categories or none]
- Mathematical-token changes: [location and exact change or none]
- Unresolved issues: [location and issue or none]
- Validation: [command/result or not run with reason]
- Coverage: [only when partial]
```

For pasted text, return corrected source first, then the same categories. For
review-only mode, order findings by mathematical/meaning-changing risk, LaTeX
errors, then language/typography. If no objective issue remains, say so and make
no change.

Referenced files: 4

View saved version →

---
name: research-attempt
description: >-
  Run one bounded, auditable mathematical research route: a proof attempt, reduction, counterexample search, source-dependent implication, or claim-supporting computation. Use when the user explicitly asks to attack a research question or invokes this skill. Do not use for a sustained multi-route investigation that continues after failed approaches, routine editing, explanation, or an unchanged verification rerun.
---

# Bounded mathematical research attempt

Pursue one route far enough to obtain a durable result, a precise obstruction,
or a well-identified next implication. This is a work-package boundary, not a
reason to stop a broader user-authorized investigation. For sustained or
multi-route requests, use the available `research-program` workflow, or continue
successive attempts directly if it is unavailable. Do not turn the log into a
transcript.

## Resolve project context

Determine the repository root first. Read the applicable `AGENTS.md`, the
current status summary when present, and only the files relevant to the target.
Search a large status, claims file, or history index for relevant sections
rather than loading it wholesale. Resolve project roles from the paths
named there. When not explicit, look for the standard alternatives in
[project-context.md](references/project-context.md). Interpret every project
path relative to the repository root, never relative to this installed
`mathbox:research-attempt` plugin skill (or its standalone installation).

If the project uses `.mathbox/`, use the available `research-state` skill's
brief check and goal handoff, opening full details only for the relevant
contracts and evidence. Check freshness and the target's dependency closure
before trusting a status label. Otherwise use the existing prose evidence records. A clean ledger
is bookkeeping evidence, not mathematical verification.

## Open the route

1. Inspect the worktree and preserve unrelated changes.
2. Normalize the target:
   - exact statement or decision;
   - quantified objects and source/target types;
   - hypotheses, coefficient domain, grading, variance, signs, finiteness,
     completion, equivariance, and range;
   - current evidence status and dependencies.
3. Search the research-history index for the target and nearby mechanisms,
   then open only the nearest relevant records needed to find the first failed
   or unproved implication.
4. State a falsifiable success criterion, a failure/no-go criterion, and the
   cheapest decisive example, source check, or computation.
5. Choose one route within the current program. Match it against prior failed
   mechanisms, not merely prior titles. Retrying a mechanism with an established
   obstruction requires a new input, invariant, construction or hypothesis that
   addresses its first failed step. An unresolved step is not an obstruction;
   resuming an untried or deferred continuation needs a concrete next action,
   not a new mathematical premise. When resuming a stalled step, state what
   differs from the stalled attempt: a narrower sub-step, method, tool or
   resource. Do not rerun it unchanged.

Use the route card in [route-card.md](references/route-card.md) when a durable
entry will be needed.

For an obstructed structural route, consult the relevant moves in
[structural-moves.md](references/structural-moves.md). Turn a proposed analogy
into a specific comparison, obstruction or discriminating invariant.

## Execute

- Begin with the smallest typed case capable of changing the conclusion.
- Verify that the chosen example, representative and every intermediate
  construction belong to the claimed domain; a convenient surrogate needs an
  explicit comparison theorem before it can decide the route.
- Search actively for counterexamples, boundary cases, convention failures,
  circularity, and missing hypotheses.
- Check nullary/unary or minimum-parameter cases and absolute degrees whenever
  a unit, augmentation, suspension or induction boundary is involved.
- Do not repair a failed type, sign, variance, normalization, or completion
  check by silently changing the statement or convention.
- Route every load-bearing question about what an external mathematical source
  proves through the available `literature-check` skill
  (`mathbox:literature-check` in plugin installations). That workflow checks an
  authorized project-local cache before fetching. If the skill is unavailable,
  perform the exact-source check directly with available tools. If the source
  cannot be verified, leave the input conditional; snippets and memory do not
  discharge it.
- For computation, separate the mathematical claim from the finite assertion
  implemented. Record domain, bounds, seed, versions, inputs, runtime, and
  non-claims; use the `mathbox:computation-audit` plugin skill when
  appropriate.
- Before calling a finite sweep exhaustive, compare the claimed population with
  the actual iterator, filters and skipped cases. Sampling requires a proved
  coverage reduction.
- After any bounded success, pause before extending the arity, range, or case
  ladder. Identify the minimal structural features used, separate uniform
  features from case-specific coincidences, and formulate the candidate
  uniform lemma or obstruction. Run another finite case only if it
  discriminates between named alternatives or enters a genuinely new regime.
- A timeout, failed search, or bounded computation is not a universal negative
  result.
- A change to a registered convention requires explicit owner approval unless
  the project instructions already authorize that exact correction.

## Classify the outcome

Use one of:

- proved as written;
- proved after an explicit restriction;
- conditional on a named unverified input;
- computationally verified only in a stated range;
- heuristic or conjectural;
- refuted, with the smallest counterexample found;
- ill-typed or incomplete;
- inconclusive, with the first unresolved implication.

State the strongest surviving result. Never upgrade evidence because the route
was long or persuasive.

Classify this attempt separately from the route's disposition. If a construction
is unresolved, say what you could not establish; do not infer that it is
impossible. Preserve other proposed continuations as untried, obstructed with
evidence, or deferred with a reason and resumption condition. An inconclusive
attempt or a resource limit alone does not close the route. Return unfinished
work to the program, or retain an executable handoff when only this bounded
attempt was authorized. Closing an unresolved route needs an account of why no
known continuation remains executable within its stated scope.

## Persist at a natural checkpoint

Exploration may remain scratch work. Create durable records when the route
produces reusable mathematics, a counterexample, a corrected dependency, a
material blocker, a convention decision, or a claim-supporting computation.

- Put reusable proof or obstruction details in the project's durable proof
  location.
- Write one self-contained route record in the project-designated research
  records directory, or `research/records/` when none is designated. Use the
  format and filename rules in [route-card.md](references/route-card.md).
- Append one compact linked entry to the project-designated route index. In a
  small flat history this is normally `RESEARCH_LOG.md`; in a sustained
  program it may be a program/phase index reached from the short top-level
  history entry point. Do not add the same route to both levels or put route
  details, commands, or dead ends in an index. If a hierarchical project has
  no designated route index, resolve that location under its edit rules before
  appending; do not turn the top-level program entry into a flat route log.
- Update live status or claim obligations only when project state changed.
- Treat live status as current state, not chronology. Keep its latest full
  verification summary and link the route record or manifests for older runs.
  Do not add another full checkpoint story. Replace a stacked dated narrative
  with current facts and a link only when that narrative already has a durable
  home (an indexed record, manifest, or closeout) and the project's edit policy
  permits it. Otherwise leave it in place and report that compaction needs a
  `research-program` closeout or `mathbox:research-init` migration.
- In an executable ledger, record only changed contracts, evidence, reviews,
  and route outcomes. A session alone needs no event. Use a prevalidated batch
  for several necessary events while preserving their distinct types.
- When persistence is authorized but this host cannot execute or write, use the
  `research-state` deferred-handoff contract for the durable files, index entry,
  and ledger proposals; report that local ingest has not yet recorded them.
- Once indexed, keep the record and index entry immutable. Record a correction
  in a new file with a `Corrects:` link and append it to the same designated
  route index. Do not create a program closeout for each attempt.
- If the index still contains legacy long-form entries, do not rewrite them as
  a side effect of this attempt. Use the new format prospectively and report
  that a `mathbox:research-init` migration remains pending.
- Do not integrate into a manuscript unless that is separately requested.

Evidence labels and promotion rules are summarized in
[evidence-model.md](references/evidence-model.md).

## Verify and report

Run the narrowest relevant documented check, then broader checks only when their
risk trigger applies. Report:

1. target and route;
2. outcome and evidence label;
3. decisive derivation, source, counterexample, or computation;
4. durable files changed;
5. commands run and exact scope;
6. unresolved assumptions and the next mathematical question; when evidence is
   bounded, include its uniform route or discriminating check.

Referenced files: 7

View saved version →

---
name: research-init
description: >-
  Initialize or migrate an AI-assisted mathematical research repository's agent architecture. Use only when the user explicitly asks to set up, plan a retrofit, or substantially revise AGENTS.md, CLAUDE.md, live research status/history, workflow files, or their authority structure, including migrating a flat research log across programs into program indexes. Inspect first, propose a reviewable file plan, and default to no repository-local skills. Do not use for an ordinary research attempt, a closeout of one named program or phase, or a read-only project retrospective.
---

# Mathematical research repository initializer

Configure the repository as a durable research environment. Do not regenerate
skills supplied by the `mathbox` plugin inside it.

## Non-negotiable behavior

- Run only after an explicit request.
- A request for a migration plan is read-only; a plugin upgrade alone does not
  authorize rewriting an existing project's files.
- Inspect before asking questions; do not ask for facts safely available in the
  repository.
- Ask at most five material questions at a time.
- Present a proposed file/migration plan before writing unless the user already
  authorized immediate execution.
- Apply the user's existing authorization to coherent setup/retrofit changes;
  do not ask again for routine edits already in scope. Preserve substantive
  existing material and show a reviewable diff. Resolve genuine ambiguity before
  replacing an authoritative proof, convention, or historical record.
- Do not invent commands, proof status, conventions, repository paths, or
  permissions.
- Preserve unrelated work. Do not commit, push, install dependencies, upload
  content, or contact third parties without authorization.
- Keep stable rules in instructions, recurring procedures in `mathbox` plugin
  skills, mutable facts in research records, and deterministic enforcement in
  code.

## Phase 1 — inspect read-only

1. Determine repository root and inspect `git status --short`. Distinguish a
   clean Git worktree from unavailable Git metadata; do not report both as an
   empty status.
2. Locate root/nested `AGENTS.md`, Claude memory/rules, current skill folders,
   and any unrecognized `skills/` folders. If root `CLAUDE.md` exists alongside
   `AGENTS.md`, check whether it imports `@AGENTS.md`. A missing `CLAUDE.md` is
   expected when Claude Code loads `AGENTS.md` directly.
3. Locate likely charter, status, claims, conventions, proof/manuscript,
   literature, log, computation, tests, CI, and build artifacts. Recognize
   semantic aliases and variants, including `PLAN`, `STATUS`, `OUTLINE`,
   `MANIFEST`, theorem/fact inventories and dated or qualified `HANDOFF` files;
   names are candidates, not authority decisions. Inventory computation
   manifests separately from build manifests. Detect project-declared path maps
   and source-cache locations, and recognizable alternate cache conventions,
   without reading cached source content or proposing a second cache by default.
   Treat theorem/fact inventory entries derived from literature as candidate
   assertions until their exact source records are checked; schedule that
   verification before dependent proof or manuscript work treats them as facts.
4. Classify the designated history entry point, often `RESEARCH_LOG.md`, as a
   compact flat index, a program-level index, long-form legacy history, or a
   mixture. Locate any program/phase route indexes and standalone records;
   check that the entry point reaches them.
   Detect `.mathbox/config.json` without replaying all history during inventory.
5. Detect duplicate `mathbox` plugin skill names and paths hard-coded relative
   to a skill installation. Report multiple dashboard or handoff candidates for
   authority review. Conservatively check relative Markdown links and
   path-shaped backtick references; distinguish certain broken links from
   tentative path candidates and ignore code fences, URLs and shell examples.
6. Run the bundled read-only inspector when available:

```bash
python3 <mathbox-research-init-directory>/scripts/inspect_repo.py --root <repo>
```

Locate the installed `mathbox:research-init` plugin skill directory (or its
standalone installation); do not substitute a guessed relative path. The
default report is a brief inventory with counts and current-path examples,
including research-log and computation-manifest classifications, project and
misplaced root skills, and build manifests. Use `--full` for the complete
Markdown report or `--format json` for complete structured data. Broken links
under archive, import, legacy, migration, or quarantine paths are counted as
historical and listed only in those full views; do not treat their location
alone as a live broken link. Links in current route records stay current. A dated
checkpoint-marker count is a prompt to inspect a long live file, not a verdict
about mathematical status or whether its history can be removed.
If current-path findings are omitted, inspect those findings in the full view
before making authority or edit decisions; a historical-only overflow need not
be loaded into the working context.

Produce a fact sheet with observed facts, tentative inferences, conflicts, and
missing information. Preserve confidence distinctions: a filename, directory
name or path-shaped code span is not proof of its semantic role.

Initialization may inventory literature records and cache policy, but it does
not establish what cited mathematics proves. Do not perform substantive source
lookups during setup; record them as follow-up work for the available
`literature-check` skill (`mathbox:literature-check` in plugin installations).
If the user also requested those source checks, execute them as a subsequent
work package within the same assignment. The setup boundary does not authorize
leaving an explicitly requested verification task unfinished.

## Phase 2 — interview adaptively

Use [interview.md](references/interview.md). Resolve only material ambiguity:
research goal, current deliverable, evidence thresholds, source authority,
fragile conventions, edit boundaries, verification, confidentiality/network,
Git policy, and definition of done.

If a manuscript or submission is the current deliverable, also resolve its
venue/template, language, audience, deadline and timezone, page-count rule and
page budget. The budget must account explicitly for front matter, bibliography,
figures/tables and contingency. Never infer these constraints from a filename,
an old draft, a generic venue norm or an approximate current page count.

Distinguish theorem goal from near-term output, proof from computation,
chain-level from derived/homology/topological claims, stable rules from mutable
status, and personal preferences from team-shared policy.

## Phase 3 — propose before writing

Present:

1. repository facts and unresolved questions;
2. proposed instruction hierarchy and source-of-truth order;
3. exact files to create, modify, move, archive, or leave untouched;
4. rules to retain, shorten, move, automate, or remove;
5. protected paths and approval boundaries;
6. verified fast, targeted, full, and manuscript checks;
7. migration risks and stale/conflicting instructions;
8. skill-layer decision from [skill-layer.md](references/skill-layer.md).
9. whether authorized literature retention needs a project-local cache and a
   tracked ignore rule, or should retain a safely identified project-declared
   alternate cache rather than creating a duplicate.
10. for a manuscript deliverable, the confirmed submission constraints and a
   complete page budget, with every unresolved item left explicitly unknown.
11. source-dependent inventory entries that remain unverified, and a literature-
    check work package ordered before any dependent claim is promoted or used.
12. for existing live-file migration, a section inventory and proposed content
    crosswalk, current ledger/pin baseline where present, and unresolved
    authority conflicts. Complete the mapping before replacing old content.

When this explicitly requested setup, retrofit, or refresh finds route-level
prose in `RESEARCH_LOG.md`, the proposed plan must include the legacy migration
below. Trigger on the log's structure, not its line count. Detection does not
authorize the rewrite.

## Existing instruction and live-state migration

For an explicit request to plan or perform migration of an existing repository's
large `AGENTS.md`, dashboard, or handoff, follow
[existing-repo-migration.md](references/existing-repo-migration.md). It defines
the baseline, content crosswalk, pin-aware edits, and before/after checks. A
plan-only request stops at the reviewed plan. Do not treat a plugin update as a
reason to rewrite a ledger, refresh hashes, or import confident prose as proof.
Use the separate legacy research-log process below if that log contains
route-level prose; use the available `research-state` skill for any optional
ledger adoption or claim/evidence revision.

## Legacy research-log migration

Make the mapping and file plan reviewable. An ordinary research attempt or
retrospective does not trigger migration. Before creating the compact index,
present a source-span-to-destination mapping to the user or designated project
owner and obtain its review. Broad retrofit authorization permits preparation
of the mapping and files, but it does not substitute for review of route
relevance or ambiguous provenance.

1. Compare each prospective entry with the repository's explicit mission,
   current target and scope. Classify it as mission-relevant, foreign, or
   ambiguous, citing the text that supports the classification. Do not infer
   relevance from a filename, topic keyword or apparent mathematical quality.
2. Map every recognizable mission-relevant route-level entry to a standalone
   record under the project-designated directory, or `research/records/` by
   default. Preserve its substantive text and chronological order; do not
   strengthen its evidence label or status.
3. Preserve foreign and ambiguous material under a project-designated
   quarantine, or `research/quarantine/legacy/` by default, with its original
   provenance and the reason it was not classified as live project history.
   Quarantine is preservation, not a mathematical verdict. Do not link this
   material from the live research index unless a reviewed mapping later
   classifies it as mission-relevant.
4. Use an entry's recorded date when available. Otherwise infer the earliest
   date from Git history that contains the entry and mark `Date provenance:
   inferred from Git history`. If Git cannot supply a date, use the migration
   date and mark that the original date was unavailable.
5. Put unmatched preamble or unstructured historical material in quarantine as
   a dated `legacy-context` record rather than discarding it. Classify it as
   mission-relevant only after review.
6. For mapping review, show source boundaries, original/inferred date, proposed
   filename, relevance class, evidence label carried forward, and any unresolved
   provenance or authority question. Revise the mapping in response to review.
7. Only after that mapping is reviewed, build a compact history entry point.
   A small project may use one chronological linked line per approved route;
   sustained programs should keep a short program/phase entry point with
   route-level indexes below it. Preserve the original flat index and its
   working links through a reviewed migration; see
   [existing-repo-migration.md](references/existing-repo-migration.md).
   Verify that every substantive part of the old log is represented in an
   indexed record, a linked unclassified-route inventory, or quarantine before
   replacing its body or changing the designated entry point. Retrospective
   closeouts distinguish the historical cutoff from their later assessment.
8. After migration, treat records and index entries as immutable. Append a new
   correction record and index entry instead of rewriting history.

## Phase 4 — write the approved project layer

Use the assets selectively; delete unused sections and replace every
placeholder. A normal setup has:

- concise root `AGENTS.md`;
- a charter stating the main question, current deliverable, success criterion,
  valuable fallback, and out-of-scope boundaries; a small project may state
  them in root `AGENTS.md` instead, but never leaves them unrecorded;
- optional `CLAUDE.md` importing `@AGENTS.md` for sessions that cannot load
  `AGENTS.md` directly or need genuine Claude-specific additions;
- at most one live dashboard;
- optional claims, conventions, literature, one compact history entry point,
  program/phase route indexes when useful, and immutable standalone records;
- when local source retention is authorized, a documented
  `.research-cache/literature/` convention and tracked Git ignore rule;
- nested instructions only for genuinely local invariants;
- documented verification commands and benchmark cases.

Do not duplicate mutable state in persistent instructions. For new setup, put
the deliverable, success criterion and fallback in the charter, and current
evidence, blocker and next action in the live dashboard. Root instructions
should point to those files and contain only stable local rules, authorization
boundaries and checks. During migration, respect existing artifact pins and
authority before moving any mutable fact. Avoid standing instructions to load
entire growing records; search for relevant contracts and history as needed.
Preserve old checkpoint material before replacing live narratives with current
state and links. Inspector size and dated-marker counts are prompts, not
authority or mathematical verdicts.
For a sustained program, keep the top-level history navigational; route lines
belong in its designated program/phase index. Project-specific size budgets
are advisory review triggers, not permission to truncate current conditions.

For a project whose claim dependencies and evidence frequently change, consider
the available `research-state` skill and its optional `.mathbox/` ledger. Use its
conservative migration workflow: import exact claims and checked artifacts,
preserve existing IDs and records, and designate a single live generated view.
Do not initialize it for a small project that does not benefit. The ledger
checks bookkeeping; it neither certifies mathematics nor replaces proof files.

For sustained multi-route work, make `research-program` discoverable as the
coordinator of successive attempts, without copying its workflow into AGENTS.

## Skill-layer rule

The default output is **no project skills**: use the installed `mathbox` plugin
for its canonical research workflows.

Never synthesize local copies of the `mathbox` plugin components
`research-attempt`, `proof-audit`, `literature-check`, `computation-audit`,
`manuscript-integrate`, `proofread-math`, `research-retrospective`, or
`research-init`, `research-program`, or `research-state`.
Never write a skill to a root `skills/` directory.

A repository skill is allowed only after explicit approval and only if its
procedure is genuinely project-specific, recurring, distinct from the canonical
catalog, and given a project-qualified name. Project facts, file paths,
mathematical hazards, and benchmark examples belong in project files instead.
If remote/team portability requires common workflows, install and pin the
`mathbox` plugin. If that host cannot load plugins, vendor exact versioned
component skills rather than rewriting them.

## Phase 5 — validate

1. Remove every placeholder.
2. Confirm each referenced path exists or is explicitly planned.
3. Confirm every command was discovered or supplied.
4. Check authority, evidence labels, Git/network rules, and edit boundaries for
   contradictions.
5. Confirm that no `mathbox` plugin skill was duplicated locally and no skill
   was put under `skills/`.
6. Check instruction size and static links/paths.
7. Review every reported dashboard/handoff candidate and broken relative path;
   do not silently choose authority or rewrite a tentative backtick candidate.
8. Confirm that any literature cache is excluded from inspection and ignored
   by a tracked project rule rather than only by the cache's own internal
   rule; do not open its source content during repository initialization.
9. Run the cheapest verified project check when authorized.
10. Inspect `git diff --check` and the full diff.
11. Tell the user how to verify loaded instructions and skills in a fresh session.
12. For a migration, reconcile the content crosswalk and compare relevant
    ledger issues, pins, claims, links, and protected instructions to baseline.

Do not commit unless explicitly authorized.

## Final report

Report files changed, hierarchy rationale, rules moved and destinations,
validation, unresolved questions/commands, `mathbox` plugin availability, any
archived duplicate skills, and one recommended namespaced plugin invocation.
For a migration, also report preserved history, unresolved authority conflicts,
and any pre-existing versus newly introduced freshness issues.

Use [output-contract.md](references/output-contract.md) as the acceptance
checklist.

Referenced files: 18

View saved version →

---
name: research-program
description: >-
  Pursue or close out a substantial mathematical research program across multiple proof, counterexample, literature, and computational routes. Use when the user asks for sustained investigation, several approaches, continuation until a goal is reached, or an authorized closeout of one named program or phase that compacts its live status and history. Coordinate successive attempts and preserve their evidence. Do not use for a single bounded lemma attempt, ordinary explanation, proofreading, a read-only project retrospective, or a repository-wide migration of instructions or a flat research log into program indexes.
---

# Sustained mathematical research

Own the user's mathematical objective across route changes. A route ending is
not the assignment ending. Produce mathematics, not a portfolio of unexecuted
suggestions. Do not promise a solution to an open problem or relabel an exhausted
attempt as one.
For a closeout-only request, reconcile recorded results and compact the handoff;
do not start new mathematical routes unless the user also requested research.
A closeout covers one named program or phase. Restructuring the repository's
history across programs, such as turning a flat research log into program
indexes, is a `research-init` migration; its closeouts follow this skill's
closeout contract.

## Establish the target once

Read project instructions, exact target, current evidence and nearest relevant
failed routes. Separate the requested theorem from weaker useful results. Fix
quantifiers, equivalence notion, coefficient regime, ranges, naturality and
conventions in a target contract. If the supplied conjecture has several
plausible meanings, work on common implications while resolving the material
ambiguity from sources or the user.

Record what would count as a proof or a counterexample and what would only be
partial progress. Retain this contract after compaction and user status queries.
“By any means” expands mathematical methods, not tool permissions or access.
For work that may cross sessions, branches or delegated agents, record a
checkpoint identifier and the exact Git revision or ledger event from which the
work starts. A timestamp or display order is not a reliable ancestry relation.

Use existing project records, starting with the current summary and nearest
relevant records rather than the complete status/history archive. When an
executable `.mathbox/` ledger is present, use the available `research-state`
skill's brief goal handoff and freshness check; open full claim/review details
only for the active decision. Before starting a run, inspect live, stale, and
unreconciled runs of the same route. Recheck stale results that bear on the
decision and reconcile completed results before relying on them. Compare a
proposed run's work scope with live runs to avoid duplicate work. Distinct
parallel runs may proceed from an explicit base with disjoint write scopes
without closing existing live runs.
Initialize it only when useful and authorized; its absence never blocks
research. Read [program protocol](references/program-protocol.md) for
route selection and checkpoints when executing routes; for a closeout-only
request, go to [program closeout](references/program-closeout.md).

## Build and execute a diverse portfolio

For a broad unresolved goal, initially identify three plausible routes unless
the user specifies another number or the problem makes fewer meaningful.
Different vocabulary for the same missing lemma is one route. Prefer routes
with different failure mechanisms; include a serious attempt to falsify the
target when a counterexample would settle it.

For each route, state the central mathematical move, its first uncertain
implication, the cheapest discriminating check, and success/failure criteria.
Treat alternative mechanisms as a portfolio and jointly required lemmas as
claim dependencies. When a route is recorded under a parent goal but directly
advances a named sub-obligation, identify that obligation explicitly rather than
retargeting the route or duplicating the mechanism.
Run the decisive check, then pursue the promising route to a substantive
checkpoint using `research-attempt` if available. Its one-route boundary applies
to each work package, not to this whole program. Follow the user's breadth
requirement: if they ask to try every proposed route, execute each one.

When routes or runs execute in parallel, give each one an owner, base
checkpoint and disjoint write scope. Require returned artifacts to identify
that base and their actual inputs. Reconcile them against the common base; do
not infer chronology or supersession from response order, directory names or
wall-clock completion.
Preserve incompatible results as competing evidence until their mathematics is
resolved.

Allocate effort by expected information gain, relevance to the goal and cost.
Do not fabricate numerical success probabilities. Attack high-impact uncertain
dependencies before polishing their downstream consequences. Formulate auxiliary
lemmas that remove shared bottlenecks. Transfer techniques across fields only
after writing the actual source-to-target dictionary.

Use `literature-check` for source-dependent implications and `computation-audit`
for load-bearing experiments. If a specialist skill is unavailable, carry out
the relevant exact-source or finite-evidence check directly with available
tools and disclose its limits; an absent workflow package is not a mathematical
obstruction.

## Change direction on evidence

After a route checkpoint, ask what mathematical information changed. Preserve
the strongest surviving statement and distinguish a false lemma, a failed
method, an implementation bug, and an inaccessible source.

- On success, extract a structural mechanism and attack the remaining gap to
  the actual goal. Do not silently replace that goal with the weaker result.
- On failure, save a reusable obstruction and revise the portfolio. A failed
  proof route does not refute the target.
- On no progress, record the first unresolved implication and distinguish the
  attempt's limits from evidence against the mechanism. Try an untested
  continuation or identify a different input, construction, invariant or source.
  Repeating a mechanism with an established obstruction requires a change that
  addresses that obstruction. Resuming unfinished work needs no new premise,
  but it must change something at the recorded stuck step: a narrower sub-step,
  another method or tool, or more resources. Do not rerun a stalled step
  unchanged; when resumptions keep stalling there, record that step as the
  route's bottleneck and reprioritize the portfolio.
- Another finite case is useful only if it distinguishes alternatives, checks
  an independent invariant, or reaches a new regime.

An inconclusive attempt does not by itself close its route. Before closing an
unresolved route, account for the proposed continuations: what was tried, what
remains untried, what evidence rules one out, and what is deferred with a reason
and resumption condition. An obstruction to one construction closes only that
construction unless it applies to the whole mechanism. Keep a route open while a plausible
continuation remains; execute it within the authorized resources or preserve it
in the handoff. A continuation that awaits time, tools, access or priority is
deferred, not exhausted; keep its route open. Reserve terminal `inconclusive`
for a scoped route whose known continuations have all been tried or ruled out
by evidence, with no further plausible continuation identified; state the scope
and reason without claiming impossibility.

Continue successive cycles while there is an executable, plausible route within
the authorized resources. Do not stop just because the initial three failed.
Likewise, a substantial partial theorem is a checkpoint, not completion, when
the target contract still contains unresolved named implications.
Use checkpoints to preserve work while continuing. When the user specifies
time/resource bounds, honor them; otherwise choose bounded individual
experiments without imposing an arbitrary global attempt quota.

## Audit candidate breakthroughs

Before treating the goal as achieved, reconstruct the complete argument from
the current definitions and pinned evidence. Check every external leaf, range,
limiting argument and comparison map. Run `proof-audit` if available.

When fresh-agent review is available and delegation is authorized, give the
reviewer the exact claim, raw proof and required sources without the author's
verdict or route narrative. Request an independent derivation of the critical
step. Otherwise perform a separate adversarial pass and label it self-review.
Agreement between agents is not a proof certificate. Resolve disagreements by
the underlying mathematics. Use [the handoff contract](references/handoff.md)
when delegating or resuming.

## Persist and report

Keep proofs in durable mathematical files, finite runs in computation records,
failed mechanisms in linked route records, and current status in one live view.
When persistence is authorized but this host cannot execute or write, use the
`research-state` deferred-handoff contract for new durable artifacts, one
guarded index entry, and ledger proposals; state that ingest remains pending.
Update only state that actually changed; replace old dashboard checkpoint prose
with links only once it has a durable home and the project permits, and do not
rewrite indexed history.
User-authorized repository deliverables remain part of completion.

At a substantial program boundary, or when the user explicitly requests
compaction, follow [program closeout](references/program-closeout.md). Produce
one linked synthesis of decisive outcomes and a small current decision view;
keep route records and ledger events intact. Closeout is not required after
every session and does not close an unresolved mathematical goal. If the
history index has become a long flat list, use the project's hierarchical
program/route index policy rather than copying all routes into the live view.
For retrospective closeout, distinguish the historical cutoff from the later
assessment; do not attribute later evidence to the old program.

For a long or externally executed route, distinguish queued, running,
last-observed, completed, failed, timed out and abandoned states. Do not keep a
route marked running merely because a prior session launched it. Record the
last observation and execution identifier without treating process completion
as mathematical success.

Lead with whether the original goal was reached and the exact result. State the
proof/review status, decisive mechanism, files and meaningful checks. If it
remains open, distinguish partial results from the goal, list executed routes
with their precise obstructions, and preserve an executable next handoff.
When all presently available routes are exhausted, or tools/resources block
every remaining continuation, say so honestly; leave blocked routes open with
their deferred next steps. Never invent progress to satisfy “do not stop”.

Referenced files: 7

View saved version →

---
name: research-retrospective
description: >-
  Reconcile a mathematical research repository's current claims, proofs, computations, status, literature dependencies, and failed routes, then recommend the next bounded research moves. Use only when the user asks for a project review, weekly/monthly retrospective, prioritization, a prose project handoff, or “what should I do next?”. Do not use to write a program closeout, migrate research history, operate a .mathbox ledger, or generate its dependency-aware handoff. Default to read-only.
---

# Research retrospective

Produce a decision-quality view of the project, not a chronological summary.
Default to no edits unless the user asks to reconcile files.

## Establish authority

1. Determine repository root and applicable instructions.
2. Resolve charter, live status, claims, conventions, literature ledger, durable
   proofs, computations, verification, research-history index, and detailed
   record directory.
   Verify that referenced live-role paths exist and expose competing aliases or
   broken authority links.
3. Read the current summary and search the compact history index for relevant
   routes. Do not load a long dashboard, claims inventory or index in full just
   to find the latest state. Open only the proof or research records needed to
   verify conflicts or load-bearing claims.
4. Do not choose a newer timestamp over stronger evidence. Expose unresolved
   authority conflicts.
5. Compare the live dashboard's review/checkpoint revision with later changes to
   authoritative manuscripts, proofs and declared deliverables. A stale date is
   a prompt to inspect, not by itself proof that the mathematics changed.

If `.mathbox/` is present, use the available `research-state` skill's brief
read-only check and goal handoff, then inspect full details for affected claims,
review conditions and routes. Use `impact CLAIM` for a named claim's
dependents and `pin-impact PATH` for the pins of a named file. Reconstruct
affected proofs from artifacts;
do not merely repeat generated labels. Do not initialize or migrate state as a
side effect of a read-only retrospective.

Do not start a broad literature search merely to complete a retrospective. If
the requested review cannot be decided without establishing what a load-bearing
external mathematical source says, route that bounded source question through
the available `literature-check` skill (`mathbox:literature-check` in plugin
installations), which checks an authorized project-local cache before fetching.
Otherwise record the unresolved source check as a candidate next route.

If `RESEARCH_LOG.md` still contains long-form legacy entries, read only the
relevant embedded entries and support a mixture of legacy prose and new links.
Report the pending `mathbox:research-init` migration, but do not perform or
require it as a precondition for the retrospective.

## Build the portfolio

For each active claim or work package, record:

- exact target and current evidence label;
- durable evidence and review status;
- load-bearing dependencies;
- first unresolved implication or smallest counterexample;
- recent route and why it succeeded or stopped;
- expected scientific value, cost, and risk;
- whether it lies on the current critical path.

Identify duplicated efforts, stale claims, abandoned routes with reusable
information, and mutable facts incorrectly embedded in instructions.
For external or long computations, distinguish the last observed process state
from current state. A launch record without a live process, scheduler result or
later observation is `unknown`, not `running`.

Group failed routes by their first failed mechanism rather than title. Identify
shared unresolved dependencies and what mathematical change would reopen each
route. Distinguish new evidence from more prose, repeated bounded cases, and
rediscovery of already recorded obstructions.

## Select next routes

Recommend at most three bounded research routes. Each must include:

- exact unresolved mathematical question;
- why it dominates nearby alternatives;
- when current evidence is bounded, the uniform route or obstruction it
  suggests;
- cheapest decisive test and, when bounded, the alternatives it distinguishes;
- success and failure criteria;
- expected durable output;
- dependencies and resource needs;
- stopping condition.

Balance one high-leverage route with lower-risk publishable or computational
work when the project permits. Do not keep a deliverable hostage to an unrelated
open flagship problem.

## Review the AI workflow

Note recurring guidance failures, false `mathbox` plugin skill triggers,
context sinks, duplicated records, non-reproducible computations, or
verification gaps. General plugin-skill bugs belong in the `mathbox` feedback
ledger; project rules belong in the repository.

Treat a live status dashboard as current state, not verification history. Flag
stacked dated verification narratives as a context sink. When reconciliation
edits are requested, keep the latest full current summary and replace older
narratives with links to immutable research records or computation manifests.
Do not rewrite indexed records or their history-index entries; append a linked
correction record when history itself needs correction.

Flag broken links to purported live dashboards, conflicts between the designated
authority and existing files, and completed deliverables still described as
unresolved. Do not repair these during a read-only retrospective; identify the
minimal reconciliation set.

## Output

Lead with a concise project verdict. Then provide:

1. claim/work-package table;
2. contradictions or stale records;
3. critical path and principal blocker;
4. recommended routes in priority order;
5. files to reconcile, only if edits were requested;
6. the single best next prompt for the `mathbox:research-attempt` plugin skill.

Referenced files: 3

View saved version →

---
name: research-state
description: >-
  Track exact mathematical claims, evidence revisions, dependency impact, audit provenance, research routes, and parallel or delayed executions in a local append-only ledger. Use when a project has a .mathbox ledger or the user asks for executable research-state tracking, stale-evidence detection, run reconciliation, or a dependency-aware handoff generated from recorded events. Do not initialize state for a casual math question, replace proof auditing with metadata validation, or write a prose project retrospective from status files.
---

# Executable research state

Use the project's existing authority rules. The ledger checks recorded evidence,
not mathematical truth. Its generated labels say only what evidence was
recorded: for example, `proof-recorded` is not a declaration that a theorem is
proved under the project's vocabulary. Review status remains separate. Apply
the project's promotion and approval policy outside this mechanical projection.

Read [ledger.md](references/ledger.md) before recording events. The portable,
standard-library helper is [research_state.py](scripts/research_state.py).
Resolve its installed location; all artifact paths are relative to the research
project supplied with `--root`, never to the installed skill.

## Read before changing state

For an existing initialized ledger, run `--root PROJECT check --summary`, then
`--root PROJECT handoff --goal CLAIM` when that goal has been registered. These default
reports are brief: they give counts, actionable IDs, and an explicit omitted
count, including runs that are live, `stale-result`, or awaiting
reconciliation. Use `--full` after the subcommand or `--json` before it when the exact
claim contract, review, route result, or complete issue list is needed. Do not
paste a full projection into the live dashboard. For an authorized new project,
create its directory, initialize and register claims first; do not run handoff
against nonexistent state. `status`, `check`, `impact`, `pin-impact`, `next`, and
`handoff` are read-only and never initialize a ledger. `--json` goes before the
subcommand.

After resolving this skill's script as `TOOL`, use this small command map:

```bash
python3 "$TOOL" --root PROJECT check --summary
python3 "$TOOL" --root PROJECT handoff --goal CLAIM
python3 "$TOOL" --root PROJECT pin-impact PATH
python3 "$TOOL" --root PROJECT record PROPOSAL.json
python3 "$TOOL" --root PROJECT record-batch PROPOSALS.json --dry-run
python3 "$TOOL" --root PROJECT record-batch PROPOSALS.json
python3 "$TOOL" --root PROJECT ingest PACKET.json --dry-run
python3 "$TOOL" --root PROJECT ingest PACKET.json
```

`pin-impact` is read-only; use it before editing a file pinned by many claims.
The two batch calls preview and then append distinct events. Read the compact
batch contract in [ledger.md](references/ledger.md) before using them.

## When state is writable only later

If the host can inspect the repository and exact ledger head but cannot execute
the helper or write project files, and persistence is authorized, follow the
[deferred handoff contract](references/deferred-handoff.md). Return one complete
`mathbox-deferred-v1` packet with every new durable artifact needed by the
proposed events, at most one guarded index entry, and a batch of proposals.
Create files and append entries only where the project's `.mathbox/config.json`
opens them to deferred packets. Pin the packet to the exact inspected ledger
event ID and hash. Use batch aliases for new event references. Never invent
event IDs, artifact hashes, timestamps, or snapshots; the local ingest command
generates them. Put the packet in the
last fenced `json` block, with no omissions or text after it. Distinguish the
mathematical finding reached from the state actually recorded: until local
ingest succeeds, say explicitly that the packet has not been applied.

Inspect the actual evidence behind important statuses. A changed proof or
dependency invalidates the affected evidence snapshot. A retracted dependency
or current counterexample record blocks downstream proofs without rewriting
history. Run `impact CLAIM` before revising a load-bearing statement.

## Record only material changes

Initialize `.mathbox/` only when the user has authorized useful project setup or
state tracking. Existing prose projects can keep their current format; the
ledger is optional. For a migration, follow [migration.md](references/migration.md).

Write a proposal JSON and use `record FILE`. A research session is not itself
an event: record only mathematical state that changed. An already registered
bounded route can close with one route-result when closure is justified;
an unfinished attempt alone does not justify closure. Program/run lifecycle
events are for work that actually spans executors, branches, delayed returns,
or sessions. Do not revise claims, repeat evidence, or add a review merely to
mirror a route record.
For several necessary events, use `record-batch FILE` after its dry-run; this
keeps the event types separate while avoiding repeated whole-journal reads.
Register exact claims before their evidence and dependencies before consumers.
When a manuscript or theorem file controls the claim wording, bind it with an
optional `statement_artifact` and locator. Evidence needs durable artifact
paths; the helper hashes them and
records all transitive claim revisions. A source record needs an exact
identifier, version, locator and translation. A computation needs its
assertion, bounds and non-claims. It never becomes a
universal proof merely because its command succeeded.

For a computation manifest that declares hashed inputs and outputs, use the
optional `manifest` field. The ledger then pins the manifest and its declared
file closure and checks that `claim_id` matches and the run completed. This is a
freshness/linkage check, not a replacement for the computation manifest
validator or an audit of the mathematical interpretation.

Record separate review events linked to the exact evidence event and a durable
report. An independence declaration must describe a real fresh review; a
different actor name alone does not establish independence. The author cannot
declare an independent audit of their own evidence. A failed review remains
active until explicitly retracted with a reason or replaced by new evidence.
Inspect the projected active review events and report paths, especially when
conditional, failed and passing reviews coexist; a one-line review label is not
a substitute for those conditions.

Whole-file bindings stale on any byte change, including typography. Prefer a
stable claim-scoped artifact when it faithfully states the authoritative claim;
use `pin-impact` to see the declared fanout of an existing whole-file pin.
Never refresh a hash on the strength of a formatting label alone.

Correct a claim by recording a new claim revision with a reason. Correct bad
evidence/reviews with a retraction and new events. Never edit/delete numbered
events, refresh hashes merely to silence a warning, or reinterpret a changed
statement as already proved. Keep proof details outside the ledger.

## Use routes to support decisions

Record a route's owning claim and, when different, the exact obligations it
`resolves`, plus its mechanism, decisive question/test, prerequisites,
success/failure criteria and rough gain/cost estimates. Keep alternative routes
distinct from jointly required claim dependencies. `next` orders ready
routes by a transparent heuristic; use mathematical judgment over its ordering.
Separate an attempt's outcome from route closure. Close a route with its exact
outcome, obstruction or scoped reason, and next question. Before closing an
unresolved route, account for known continuations and explain why none remains
executable within the route's stated scope. An inconclusive attempt, resource
limit or priority change alone does not justify closure. Keep untried or
deferred continuations in the route record and current handoff with their next
steps and resumption conditions. Reopening a closed route requires its prior
result and a `changed_input` addressing any recorded obstruction; resuming an
open route's unfinished work does not require a new mathematical input.

For sustained or parallel work, record a program and a distinct route run for
each executor. Pin the ledger base event and external revision at which each run
started; observations supply the last-seen revision, and run results close or
abandon executions without automatically closing the mathematical route.
Reconcile an inconclusive run with `continue` when the route remains open,
including when its next action is deferred; `next` and `handoff` show that
reconciliation's next step and reason under the route. A later run uses the
same route ID. A route event cannot hold a deferred step: when a ledger route's
unfinished continuation must survive to a later session, record the attempt as
a run with its result and a `continue` reconciliation. A prose record alone
leaves the generated handoff showing only the route's original question. Do not
add run events to mirror an attempt whose follow-up finishes in the same
session. To correct an earlier premature closure that recorded no obstruction,
use the append-only reopening contract in [ledger.md](references/ledger.md);
identify the overlooked continuation rather than inventing new mathematics.
Relabelling a `failed` result or recorded obstruction as premature does not
reopen it.
Reconcile completed runs serially in the one writer's ledger. Record conflicts
and give delayed results an explicit late disposition rather than reconstructing
or merging numbered event streams. See [ledger.md](references/ledger.md) for the
event contracts.

## Report and persist

Commit ledger events with the corresponding proof/source/report artifacts only
under the project's Git authorization. Keep licensed/private source caches
under their own existing retention policy; the ledger stores references only.
Do not create a second manually maintained claims dashboard. Prefer a generated
view in the designated live status location when migration is authorized.

Report changed claims, active review conditions and conflicts, stale evidence,
affected dependents, and route-only context kept outside the theorem dependency
graph. A clean `check` means bookkeeping integrity and current artifact hashes,
not a proof audit.
For genuine correctness decisions, use the mathematical specialist workflow.

Referenced files: 8