morankor/theorist-toolbox/co-math-init

co-math-init

Author: Moran Koren, Ben-Gurion University of the Negev (korenmor@bgu.ac.il). Part of the Theorist Toolbox.

Bootstrap a new research project for the personal AI co-mathematician system, modelled after the Google DeepMind AI Co-Mathematician paper (Zheng et al., 2026-05-07).

This skill creates the directory layout, copies the LaTeX template, initializes the per-project hook configuration, and sets up the workstream registry. After init, the user can spawn workstreams via the project-coordinator sub-agent.

When to invoke

Trigger phrases:

• /co-math-init
• "start a new co-math project"
• "init a research project"
• "new mathematician project"

Steps

1. Gather inputs from the user

Ask via AskUserQuestion:

1. Project name — short, lowercase-kebab-case (e.g., ambidextrous-sofa). This becomes the directory name.
2. Initial research question — one sentence. Goes into goals.md. The user can refine later.
3. Strict mode — strict (default) or pragmatic. Strict means the prover sub-agent must mark every gap with \unproven{...} and never hand-wave. Pragmatic allows informal prose for minor steps. Default is strict unless the user explicitly says otherwise; this default is recorded in user memory and must be respected.
4. Parent directory — where to create the project. Default: current working directory.

2. Create the directory structure

Inside <parent>/<project-name>/:

paper.tex
goals.md
decisions.md
PROJECT_README.md
co-math-config.json
workstreams/
  .gitkeep
references/
  .gitkeep
failed-explorations/
  .gitkeep
.co-math/
  approvals/
    .gitkeep
  workstream-registry.json
.claude/
  settings.json        # per-project hooks (Phase 3 — empty for now)

3. Populate files from templates

Templates live in this skill's templates/ directory. For each entry below, Read the template, do placeholder substitution, then Write to the project path:

Placeholders to substitute in each file:

4. Initialize the workstream registry

Write .co-math/workstream-registry.json:

{
  "project": "<project-name>",
  "created": "<DATE>",
  "strict_mode": <true|false>,
  "next_id": 1,
  "workstreams": []
}

5. Print next steps to the user

After scaffolding, output a concise message:

• Confirm the directory was created (with absolute path).
• Explain the files: goals.md for refining the question, paper.tex is the living working paper, workstreams/ will fill up as the project-coordinator spawns work.
• Tell them to invoke the project-coordinator sub-agent (once Phase 2 ships) to start the first workstream, OR — if Phase 2 isn't built yet — to manually edit goals.md and start drafting in paper.tex.
• Note that hooks are not yet wired up (Phase 3 deliverable).
• Note the verification ladder available to the coordinator: an informal prover proof (\unproven{} for any gap), or — for results worth machine-checking — a lean-prover workstream that formalises the lemma in Lean 4 and verifies it with lake build, closing the theorem with \leanproved{W{NNN}}. After any proof is APPROVED, a proof-readability pass can polish the exposition without touching the mathematics.

Standard workstream pipeline (including the readability pass)

Every project scaffolded by this skill commits to the following pipeline for any result that is proved. The scaffolding encodes it in co-math-config.json (review_policy.require_readability_pass_after_proof) and documents it in the project README.md; the project-coordinator enforces it.

prover / lean-prover   →   paper-reviewer (correctness/acceptance)
        │                            │
        │                            ▼
        │                  Phase 4.5: readability pass
        │                  W{NNN}-readability-{slug}
        │                  (prover in readability mode, per the
        │                   `proof-readability` skill — exposition only,
        │                   never changes the mathematics)
        │                            │
        │                            ▼
        │                  paper-reviewer re-checks for content
        │                  preservation + plumbing only
        ▼                            ▼
   workstream cannot be marked COMPLETE until the readability
   pass has run and been re-approved

Rules the coordinator must follow:

• After a prover or lean-prover workstream is APPROVED, dispatch a

W{NNN}-readability-{slug} workstream before marking the proving workstream complete. Its instructions.md names exactly the approved theorems/lemmas in scope and points the executing agent at the proof-readability skill.

• The readability pass is exposition only: it must never strengthen, weaken,

or replace any claim. If it surfaces a suspected gap, the workstream returns to prover (it does not patch the math).

• paper-reviewer re-reviews the readability output for *content preservation

and plumbing* (statement preservation, references resolve, paper compiles) — not for re-proving.

• A proving workstream's complete state is gated on the readability pass having

run and been re-approved. (In strict_mode, this gate is mandatory; in pragmatic mode it may be downgraded to a recommendation, recorded in decisions.md.)

Skip the readability pass only for workstreams that produce no proof (literature surveys, pure computational evidence with no analytic claims).

What this skill does NOT do

• It does not start any workstream itself. That is the project-coordinator sub-agent's job.
• It does not invoke any agent. Pure scaffolding.
• It does not modify global Claude Code settings, only writes a per-project .claude/settings.json.

Notes on respecting prior user decisions

The default strict_mode value is always strict. If the user has previously asked to relax this for a specific project, that is recorded in that project's decisions.md, not as a global default. Each new project starts strict.