How to use the Proof Checker agent skill

What is an agent skill and what does proof-checker make the agent do?

An agent skill is a folder containing a SKILL.md file that tells a compatible agent how to carry out a specific workflow. Once installed, the agent loads the skill when a request matches the skill's description.

When you ask the agent to check a proof, proof-checker has the agent read a LaTeX proof and look for logical gaps and unjustified steps. The proof is then sent to a separate AI model acting as an adversarial reviewer. The agent fixes each flagged gap with fuller derivations, has the reviewer re-check the fixes, and produces an audit report that tracks each issue.

The skill uses a fixed issue taxonomy with 20 categories in four groups, covering logic and proof structure, analysis and measure theory, model and parameter tracking, and similar concerns. It also applies an objective pass/fail acceptance gate: the proof passes only when there are zero open FATAL or CRITICAL issues, every theorem and lemma has explicit hypotheses and justified interchanges, big-O statements declare their parameter dependence, and a counterexample pass has been run on key lemmas.

How do you install the proof-checker skill?

Download the ZIP for the skill from the directory page. Then choose one of two routes.

For a personal install, unzip the download into ~/.claude/skills/. For a project-only install, unzip it into the .claude/skills/ folder of your project.

Alternatively, if you use the Claude apps, upload the skill under Settings → Capabilities → Skills.

• Personal: unzip into ~/.claude/skills/
• Project: unzip into .claude/skills/ inside your project
• Claude apps: Settings → Capabilities → Skills, then upload

Which requirements do you need before running it?

The skill needs a reviewer backend. By default it uses the Codex MCP server as the external reviewer. You can instead configure another reviewer MCP such as oracle-pro, or manual review. If the manual-review MCP is unavailable, the skill stops and prints the install command rather than falling back to Codex.

The agent must be Claude Code or another agent that reads SKILL.md and has the listed MCP tools available. If you want a PDF audit report, you also need a LaTeX toolchain.

The skill runs scripts and uses the network, so review the safety notes below before you install it.

• External reviewer backend: Codex MCP server (default), or oracle-pro, or manual review
• Agent: Claude Code or another SKILL.md-compatible agent with the MCP tools
• LaTeX toolchain only if you want the PDF audit report

How do you trigger the skill with a natural request?

You do not need to type a command. The skill is triggered when you make a request that matches its description. Phrases listed in the description include "verify proof", "proof check", "check this proof", and "检查证明" and "审证明". You can also ask for rigorous mathematical verification of a theory paper in general terms.

You can point the agent at a .tex file or describe the proof. The skill accepts optional flags --deep-fix and --restatement-check, which are listed in its argument hint.

• "Verify proof of Lemma 3 in sections/appendix.tex"
• "Proof check this theorem and write an audit report"
• "Check this proof for gaps before I submit"

What safety and privacy points should you know?

The reviewer backend receives the proof content. If your proof text is confidential and cannot be sent to an external reviewer model, do not use this skill.

The skill runs scripts and uses the network. Its reviewer routing is set so that the reviewer model must be a non-Claude model, because the executor is Claude and the cross-model check depends on that separation. Read SKILL.md before installing to see exactly which tools it is allowed to use.

The skill is multi-round and slow, and it relies on LLM review rather than a formal proof assistant. It does not replace formal machine verification.

• Proof text is sent to the external reviewer backend
• Scripts run and network is used
• Reviewer must be a non-Claude model for the cross-model check

What tips help you get useful results?

Give the skill a specific theorem or lemma, with the file path if you have one. Check the audit document after each run, since it logs which gaps were found and how each was closed.

Do not wrap the skill in /loop, /schedule or CronCreate. The skill is verdict-bearing and keeps the reviewer's memory across rounds in one thread, which a repeating timer would reset.

• Name the exact lemma or theorem you want checked
• Keep the audit document as a record of what changed
• Do not run the skill on a recurring timer