Proof Writer

wanshuiyin/auto-claude-code-research-in-sleep

This writes formal mathematical proofs for ML and AI theory with an emphasis on intellectual honesty over polish. It triages whether claims are actually provable before attempting them, builds explicit dependency maps, and refuses to paper over gaps with "clearly" or "obviously." When a theorem statement is too strong, it tells you why and either weakens the claim or identifies the missing assumption needed to complete the proof. Outputs to a structured markdown file with status, assumptions, strategy, and numbered steps. The workflow is thorough, maybe verbose for quick sketches, but valuable when you need a proof that will survive peer review or when formalizing something that might have subtle holes.

skills.sh installs: 545
GitHub stars: 18.9K
last updated: Aug 21, 2026

View on GitHub

Install

$ npx -y skills add wanshuiyin/auto-claude-code-research-in-sleep --skill proof-writer --agent claude-code

Installs into .claude/skills of the current project.

Files

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:

a complete proof of the original claim
a corrected claim plus a proof of the corrected claim
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.