agentleFS
ImmortalqxImmortalqx/my_codex_skills/proof-writer/SKILL.md

proof-writer

Skill54 starsChanged 5 months agoMITView on GitHub

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, \u8865\u5168\u8bc1\u660e, \u5199\u8bc1\u660e, \u8bc1\u660e\u67d0\u4e2a\u547d\u9898, or determine whether a claimed proof can actually be completed under the stated assumptions.

8 other projects use a version of this, 7 of them edited.

Adopted by

Most recently taken up by

The file

Show its rules and text

We split this skill into the rules it gives an agent

16 rules. 9 are common, 4 are distinctive, and 3 are very specific to this project.

  • 9

    Common

    Most of the 7 edited versions we read keep these.

  • 4

    Distinctive

    This author's own choices. Worth a look.

  • 3

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  1. Common:

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

    line 8
  2. Common:

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

    line 25
  3. Distinctive:

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

    line 31
  4. Distinctive:

    Check explicitly: - does the conclusion actually follow from the listed assumptions?

    line 43
  5. Common:

    If the claim is not provable as stated, do NOT fabricate a proof.

    line 45
  6. Common:

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

    line 51
  7. Distinctive:

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

    line 55
  8. Very specific:

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

    line 57
  9. Very specific:

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

    line 59
  10. Common:

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

    line 67
  11. Common:

    Write the target proof file using this structure:

    line 71
  12. Distinctive:

    After writing the target proof file, respond briefly with: - status - whether the original claim survived unchanged - what file was updated

    line 119
  13. Common:

    Never fabricate a missing proof step.

    line 123
  14. Common:

    Prefer weakening the claim over overclaiming.

    line 124
  15. Common:

    If the statement is false as written, say so explicitly and give a counterexample or repaired statement.

    line 127
  16. Very specific:

    If uncertainty remains, mark it explicitly in Open Risks.

    line 128

“Common” is measured: kept by at least 6 in 10 of the 7 edited versions of this file we could read. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
SKILL.md

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

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

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

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

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

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

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

If the original claim is too strong

If the proof cannot be completed honestly

Chat Response

After writing the target proof file, respond briefly with: - status - whether the original claim survived unchanged - what file was updated

Key Rules

  • Never fabricate a missing proof step.
  • Prefer weakening the claim over overclaiming.
  • Separate assumptions, derived facts, heuristics, and conjectures.
  • Preserve the user's original theorem statement unless you explicitly mark a corrected claim or an internal normalization.
  • If the statement is false as written, say so explicitly and give a counterexample or repaired statement.
  • If uncertainty remains, mark it explicitly in Open Risks; do not hide it inside polished prose.
  • Correctness matters more than brevity.

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.