Mmcp.market

proof-writer skill

by wanshuiyin·wanshuiyin/Auto-claude-code-research-in-sleep·17k stars·MIT

Writes rigorous mathematical proofs for ML/AI theory. Use when asked to prove a theorem, lemma, proposition, or corollary, fill in missing proof steps, formalize a proof sketch, 补全证明, 写证明, 证明某个命题, or determine whether a claimed proof can actually be completed under the stated assumptions.

A100/100content scan

Is the proof-writer skill safe?

Clean: nothing in its files matched our rules. We read 1 file in the folder on 2026-09-28.

No findings.

Install the proof-writer skill

A skill is a folder. Copy it into your agent's skills folder and the agent loads it when the task matches its description.

git clone --depth 1 https://github.com/wanshuiyin/Auto-claude-code-research-in-sleep.git /tmp/Auto-claude-code-research-in-sleep
mkdir -p ~/.claude/skills
cp -r /tmp/Auto-claude-code-research-in-sleep/skills/proof-writer ~/.claude/skills/proof-writer
available in every project

In the Claude apps, zip the folder and upload it from the Skills settings. The folder on GitHub

The instructions your agent would load

SKILL.md as published, without the frontmatter. Read it on GitHub

Proof Write: Rigorous Theorem / Lemma Drafting

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

Constants

  • DEFAULTPROOFDOC = 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.

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

If the user does not specify a target, default to PROOF_PACKAGE.md in project root.

Do NOT write directly into paper sections or appendix .tex files unless the user explicitly asks for that target.

The proof package must include:

  • exact claim
  • explicit assumptions
  • proof status
  • announced strategy
  • dependency map
  • numbered major steps
  • justification for every nontrivial implication

Mathematical rigor requirements:

  • never use "clearly", "obviously", "it can be shown", "by standard arguments", or "similarly" to hide a gap
  • define every constant and symbol before use
  • check quantifier order carefully
  • handle degenerate and boundary cases explicitly, or state why they are excluded
  • if invoking a standard fact, state its name and why its assumptions are satisfied here
  • use $...$ for inline math and $$...$$ for display equations
  • never write math in plain text
  • if the proof uses an equivalent normalization that is stronger in appearance than the user's original theorem statement, label it explicitly as a proof device and keep the original claim separate

Step 6: Final Verification

Before finishing the target proof file, verify:

  • the theorem statement exactly matches what was actually shown
  • every assumption used is stated
  • every nontrivial implication is justified
  • every inequality direction is correct
  • every cited result is applicable under the stated assumptions
  • edge cases are handled or explicitly excluded
  • no hidden dependence on an unproved lemma remains

If a key step still cannot be justified, downgrade the status and write a blockage report instead of forcing a proof.

Required File Structure

Write the target proof file using this structure:

# Proof Package

## Claim
[exact statement]

## Status
PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED

## Assumptions
- ...

## Notation
- ...

## Proof Strategy
[chosen approach and why]

## Dependency Map
1. Main claim depends on ...
2. Lemma A depends on ...
3. Step k uses ...

## Proof
Step 1. ...
Step 2. ...
...
Therefore the claim follows. ∎

## Corrections or Missing Assumptions
- [only if needed]

## Open Risks
- [remaining fragile points, if any]

Output Modes

If the claim is provable as stated

Write the full file structure above with a complete proof.

If the original claim is too strong

Write:

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

  • Aablation-plannerUse when main results pass result-to-claim (claim_supported=yes or partial) and ablation studies are needed for paper submission.
  • Aablation-plannerUse when main results pass result-to-claim (`claim_supported = yes` or `partial`) and ablation studies are needed for paper submission. A secondary Codex agent designs ablations from a reviewer's perspective; the local executor reviews feasibility and implements.
  • AalphaxivQuick single-paper lookup via AlphaXiv LLM-optimized summaries with tiered source fallback. Use when user says "explain this paper", "summarize paper", pastes an arXiv/AlphaXiv URL, or provides a bare arXiv ID for quick understanding - not for broad literature search.
  • AalphaxivQuick single-paper lookup via AlphaXiv LLM-optimized summaries with tiered source fallback. Use when user says "explain this paper", "summarize paper", pastes an arXiv/AlphaXiv URL, or provides a bare arXiv ID for quick understanding - not for broad literature search.
  • Aanalyze-resultsAnalyze ML experiment results, compute statistics, generate comparison tables and insights. Use when user says "analyze results", "compare", or needs to interpret experimental data.
  • Aanalyze-resultsAnalyze ML experiment results, compute statistics, generate comparison tables and insights. Use when user says \"analyze results\", \"compare\", or needs to interpret experimental data.
  • AarxivSearch, download, and summarize academic papers from arXiv. Use when user says "search arxiv", "download paper", "fetch arxiv", "arxiv search", "get paper pdf", or wants to find and save papers from arXiv to the local paper library.
  • AarxivSearch, download, and summarize academic papers from arXiv. Use when user says \"search arxiv\", \"download paper\", \"fetch arxiv\", \"arxiv search\", \"get paper pdf\", or wants to find and save papers from arXiv to the local paper library.
  • Aauto-paper-improvement-loopAutonomously improve a generated paper via GPT-6-Astra xhigh review → implement fixes → recompile, for 2 rounds. Use when user says \"改论文\", \"improve paper\", \"论文润色循环\", \"auto improve\", or wants to iteratively polish a generated paper.
  • Aauto-paper-improvement-loopAutonomously improve a generated paper via Claude review through claude-review MCP → implement fixes → recompile, for 2 rounds. Use when user says \"改论文\", \"improve paper\", \"论文润色循环\", \"auto improve\", or wants to iteratively polish a generated paper.
  • Aauto-paper-improvement-loopAutonomously improve a generated paper via Gemini review through gemini-review MCP → implement fixes → recompile, for 2 rounds. Use when user says \"改论文\", \"improve paper\", \"论文润色循环\", \"auto improve\", or wants to iteratively polish a generated paper.
  • Aauto-paper-improvement-loopAutonomously improve a generated paper via GPT-6-Astra xhigh review → implement fixes → recompile, for 2 rounds. Use when user says \"改论文\", \"improve paper\", \"论文润色循环\", \"auto improve\", or wants to iteratively polish a generated paper.

All agent skills → · MCP servers