菜单
Formalize a natural-language mathematical proof in Lean 4 (or another kernel) incrementally: small goals first, expand, audit mismatches, refactor. Use after an informal proof of an open problem is drafted and audited, or when the user asks for Lean formalization of a proof artifact.
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt；运行前请先检查来源。
npx skills add https://github.com/meleantonio/prove-that-shit --skill formalize-proof命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地？可下载 SkillsMP 当前能够提供的文件。
Independently attack a candidate mathematical proof: find gaps, circular lemmas, silent hypothesis changes, insufficient uniformity, and false completions. Use after any draft proof of an open problem, before claiming success, or when the user asks to audit, stress-test, or red-team a proof.
Build a problem-specific open-problem proof prompt that defines success, bans weaker substitutes, lists traps, and configures multi-agent adversarial search. Use when preparing Codex/Cursor/Claude goals for proving or disproving a conjecture, or when asked to generate prompts in the Wang/OpenAI cycle-double-cover style.
Attack an open mathematical problem end-to-end using the Wang/Codex Erdős workflow: select tractability, craft a problem-specific proof prompt, run a long attempt→audit→repair research loop with multi-agent search, and emit LaTeX/Python/Lean artifacts. Use when the user asks to prove, disprove, resolve, or attack an open math problem (Erdős, conjectures, research questions), or when they mention prove-that-shit / open-problem proving.
基于 SOC 职业分类
正在显示 SKILL.md
| name | formalize-proof |
| description | Formalize a natural-language mathematical proof in Lean 4 (or another kernel) incrementally: small goals first, expand, audit mismatches, refactor. Use after an informal proof of an open problem is drafted and audited, or when the user asks for Lean formalization of a proof artifact. |
Follow-on to a successful informal resolution. Formalization is optional for claiming an informal win, but it is the strongest machine check available.
lake, mathlib as needed). Do not assume the
user already has Lean./goal (or equivalent): formalize one lemma or section.adversarial-proof-audit) before forcing Lean.If available, use a second coding agent to audit Lean code vs the paper for:
sorry / admit / unchecked axioms;problems/<id>/lean/
lakefile.toml / lakefile.lean
Main.lean
...
FORMALIZATION_NOTES.md
Record in STATUS.md whether formalization is complete, partial, or pending.