Proof Usage
Overview
Use this skill as the final agent-facing proof playbook. It stores cooked entries synthesized from proof-material, not raw source extraction notes.
Start at references/index.md. The index routes by problem shape, assumptions, desired proof move, tags, and source material IDs.
Pipeline Position
proof-usage is the final lookup stage:
proof-cooker -> proof-usage -> current proof task
Its job is usability. A theorem-proving agent should search this playbook first, apply a cooked entry when assumptions match, and follow material IDs back to proof-material only when source-level context is needed.
Library Modules
- references/index.md: first stop for routing and search.
- references/source-map.md: maps cooked entries back to stable proof-material IDs and public sources.
references/local-moves/: local lemmas, estimates, concentration steps, convexity conversions, parameter balances, and restart controls.references/strategies/: macro proof architectures, auxiliary-model arguments, staged algorithms, and role-separation templates.- references/techniques.md and references/strategies.md: legacy compatibility files retained while older cards are migrated or linked.
Usage Workflow
- Parse the user's proof target.
- Identify the object being bounded, constructed, localized, decomposed, or compared.
- Note assumptions such as linearity, convexity, error-bound conditions, bounded features, filtration, Bellman structure, duality, or self-normalized processes.
- Search the index.
- Match by task shape first, then assumptions, desired move, tags, and material IDs.
- Load only the category files that match the current proof target.
- Adapt the cooked entry.
- Translate notation into the user's setting.
- Check required assumptions and failure modes before using the move.
- Follow
Material sources back to proof-material only when source-level details are needed.
- Be honest about fit.
- If a move requires stronger assumptions than the user has, say so.
- If no entry fits, explain the closest partial analogy and what additional lemma would be needed.
Cooked Entry Contract
Each cooked entry should include:
CategoryUse whenRequired assumptionsCore moveSelf-contained statement or templateHow to adaptFailure modesRelated entriesMaterial sourcesPublic attribution
Maintenance
proof-cooker owns taxonomy updates, de-duplication, source-map maintenance, and migration from legacy files.- Cooked entries must link to one or more stable material IDs.
- Keep raw extraction notes, DeepSeek transcripts, local OCR dumps, source-local clutter, private paths, account names, and unpublished project details out of this skill.
1---2name: proof-usage3description: Look up and apply the cooked, indexed proof playbook built from proof-material. Use when the user is proving a theorem, planning a proof, seeking reusable proof moves by task shape, assumptions, tags, desired move, or material source ID, or adapting cooked local moves and macro strategies with public source attribution.4---56# Proof Usage78## Overview910Use this skill as the final agent-facing proof playbook. It stores cooked entries synthesized from `proof-material`, not raw source extraction notes.1112Start at [references/index.md](references/index.md). The index routes by problem shape, assumptions, desired proof move, tags, and source material IDs.1314## Pipeline Position1516`proof-usage` is the final lookup stage:1718```text19proof-cooker -> proof-usage -> current proof task20```2122Its job is usability. A theorem-proving agent should search this playbook first, apply a cooked entry when assumptions match, and follow material IDs back to `proof-material` only when source-level context is needed.2324## Library Modules2526- [references/index.md](references/index.md): first stop for routing and search.27- [references/source-map.md](references/source-map.md): maps cooked entries back to stable proof-material IDs and public sources.28- `references/local-moves/`: local lemmas, estimates, concentration steps, convexity conversions, parameter balances, and restart controls.29- `references/strategies/`: macro proof architectures, auxiliary-model arguments, staged algorithms, and role-separation templates.30- [references/techniques.md](references/techniques.md) and [references/strategies.md](references/strategies.md): legacy compatibility files retained while older cards are migrated or linked.3132## Usage Workflow33341. Parse the user's proof target.35 - Identify the object being bounded, constructed, localized, decomposed, or compared.36 - Note assumptions such as linearity, convexity, error-bound conditions, bounded features, filtration, Bellman structure, duality, or self-normalized processes.372. Search the index.38 - Match by task shape first, then assumptions, desired move, tags, and material IDs.39 - Load only the category files that match the current proof target.403. Adapt the cooked entry.41 - Translate notation into the user's setting.42 - Check required assumptions and failure modes before using the move.43 - Follow `Material sources` back to `proof-material` only when source-level details are needed.444. Be honest about fit.45 - If a move requires stronger assumptions than the user has, say so.46 - If no entry fits, explain the closest partial analogy and what additional lemma would be needed.4748## Cooked Entry Contract4950Each cooked entry should include:5152- `Category`53- `Use when`54- `Required assumptions`55- `Core move`56- `Self-contained statement or template`57- `How to adapt`58- `Failure modes`59- `Related entries`60- `Material sources`61- `Public attribution`6263## Maintenance6465- `proof-cooker` owns taxonomy updates, de-duplication, source-map maintenance, and migration from legacy files.66- Cooked entries must link to one or more stable material IDs.67- Keep raw extraction notes, DeepSeek transcripts, local OCR dumps, source-local clutter, private paths, account names, and unpublished project details out of this skill.
shenmuxing