proof-writer

Files (1)

• SKILL.md

SKILL.md (first lines)

# Proof Write: Rigorous Theorem / Lemma Drafting

Write a mathematically honest proof package, not a polished fake proof.

## Constants

- DEFAULT_PROOF_DOC = `PROOF_PACKAGE.md` in project root
- STATUS = `PROVABLE AS STATED | PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION | NOT CURRENTLY JUSTIFIED`

## Context: $ARGUMENTS

## Goal

Produce exactly one of:
1. a complete proof of the original claim
2. a corrected claim plus a proof of the corrected claim
3. a blockage report explaining why the claim is not currently justified

## Inputs

Extract and normalize:
- exact theorem / lemma / proposition / corollary statement
- explicit assumptions
- notation and definitions
- any user-provided proof sketch, partial proof, or intended strategy
- nearby lemmas or claims in local notes, appendix files, or theorem drafts if the request points to them
- desired output style if specified: concise, appendix-ready, or full-detail

If notation or assumptions are ambiguous, state the exact interpretation you are using before proving anything.

## Workflow

### Step 1: Gather Proof Context
Determine the target proof file with this priority:
1. a file path explicitly specified by the user
2. a proof draft already referenced in local notes or theorem files
3. `PROOF_PACKAGE.md` in project root as the default target

Read the relevant local context:
- the chosen target proof file, if it already exists
- theorem notes, appendix drafts, or files explicitly mentioned by the user

Extract:
- exact claim
- assumptions
- notation
- proof sketch or partial proof
- nearby lemmas that the draft may depend on

### Step 2: Normalize the Claim
Restate:
- the exact claim being proved
- all assumptions, separately from conclusions
- all symbols used in the claim

Identify:
- hidden assumptions
- undefined notation
- scope ambiguities
- whether the available sketch proves the full claim or only a weaker variant

Preserve the user's original theorem statement unless a change is explicitly required.
If you use a stronger normalization or cleaner internal formulation only to make the proof easier, keep that as an internal proof device rather than silently replacing the original claim.

### Optional Lean proof route

When the user requests Lean, or formalizing a specific proof obligation would
materially help establish correctness, invoke
[`/lean-formalize`](../lean-formalize/SKILL.md) with the original statement,
current attempt, and known dependencies. It develops the proof as well as its
formal implementation. Return the checked scope, exported theorem and remaining
obligations to this proof package. A partial result closes only its corresponding
obligation. When called by `lean-formalize` to develop a missing mathematical
argument, return that argument and remaining gaps to the calling Lean run;
do not invoke `lean-formalize` recursively. Ordinary proof drafting does not
require Lean; difficulty alone does not trigger it.

### Step 3: Feasibility Triage
Before writing a proof, classify the claim into exactly one status:
- `PROVABLE AS STATED`
- `PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION`
- `NOT CURRENTLY JUSTIFIED`

Check explicitly:
- does the conclusion actually follow from the listed assumptions?
- is any cited theorem being used outside its conditions?
- is the claim stronger than what the available argument supports?
- is there an obvious counterexample, boundary case, or quantifier failure?

If the claim is not provable as stated, do NOT fabricate a proof.
Do NOT silently strengthen assumptions or narrow the theorem's scope just to make the proof work.

### Step 4: Build a Dependency Map
Choose a proof strategy, for example:
- direct
- contradiction
- induction
- construction
- reduction to a known result
- coupling / probabilistic argument
- optimization inequality chaining

Then write a dependency map:
- main claim
- required intermediate lemmas
- named theorems or inequalities that will be cited
- which assumptions each nontrivial step depends on
- boundary cases that must be handled separately

If one step is substantial, isolate it as a lemma instead of burying it in one sentence.

### Step 5: Write the Proof Document
Write to the chosen target proof file.

If the target proof file already exists:
- read it first
- update the relevant claim section
- do not blindly duplicate prior content

From wanshuiyin/Auto-claude-code-research-in-sleep, MIT.

More from wanshuiyin/Auto-claude-code-research-in-sleep