# Verify Proof > Verify a result and, on acceptance, write it as a fact — via the fact_submit tool. Use for the full target theorem AND for every sharply-delimited intermediate result, lemma, construction, or formula you intend to build on. The verifier is the sole authority on mathematical correctness. - Skill: `frenzymath/verify-proof` (Agent Skill, multi-file: 2 files) - Install (CLI): `npx skillmds@latest add frenzymath/verify-proof` - Raw SKILL.md: https://api.skillmd.com/api/skills/frenzymath/verify-proof/raw - Safety review: pending - Works with: Claude Code, Claude.ai, OpenAI Codex - Category: Coding & Dev Tools, AI & ML - Author: frenzymath (https://skillmd.com/u/frenzymath) - Updated: 2026-09-17 - Page: https://skillmd.com/skills/frenzymath/verify-proof --- # Verify Proof The verifier is the **canonical and sole authority on mathematical correctness**. Mathematics requires 100% accuracy; even though this verifier is not a formal proof assistant, it is the strongest correctness check in the system. No LLM consultation, panel, or self-critique substitutes for it. **You verify and write a fact through one tool: `fact_submit`.** It runs the glossary-coverage check, calls the verifier, and writes the fact to the fact graph **iff the verifier accepts** — there is no other way a fact enters the graph. ## When to submit - **The full target theorem** — when you have assembled a complete proof of the whole problem (as a self-contained statement + proof, citing its predecessors by `fact_id`). - **Every intermediate result you intend to USE downstream** — a lemma, a candidate construction, an arithmetic/closed-form claim, a saturation or local-to-global claim, any sharply-delimited step. **Adopting an unverified partial result as a building block is the single biggest correctness risk.** When in doubt, submit. Choose a substantive mathematical boundary, not the smallest checkable line. Routine calculations, substitutions, and bookkeeping identities should normally remain internal steps in the proof of a deeper fact. The submitted fact should state one mathematically significant conclusion; depth must not be simulated by bundling several shallow or unrelated claims. Split supporting claims only when they have independent downstream uses, separate proof obligations, or need isolated verifier repair. Do **not** build on an unverified finding from global memory. A `conclusion` / `example` / `counterexample` there is awareness, not a brick — re-derive it as a self-contained statement+proof and submit it before relying on it. ## Before you submit — write an "ugly-proof" fact A fact in the fact graph is written in **"ugly-but-rigorous"** form (the operator may call it an **"ugly-proof"**). The one goal of this form is that the fact is **mechanically checkable for correctness** by a reader with no memory and no math intuition (an agent with no recall, a human, the verifier). It is allowed — encouraged — to be **ugly**: redundant, machine-flavored, verbose. It is **not allowed** to be ambiguous, vague, or context-dependent. "Ugly" is the deliberate contrast with the polished arXiv paper (a separate pipeline); here, only mechanical correctness matters. Concretely, before you submit: - **Self-contained.** A reader using only this fact + its declared predecessors + the project glossary can decide whether the math is correct. No appeal to chart positions, parse status, project history, or "as we know". - **Define every symbol.** Each symbol used in the statement/proof is defined: in this fact's `glossary_introduces`, in a cited predecessor's glossary, in the project glossary, or in the **global glossary** of universal notation (Z, Q, R, C, floor/ceil, gcd/lcm, intervals, Greek parameter names). Don't redefine universal notation — `glossary_introduces` is for project-specific symbols only. Reuse the project's existing symbol for the same object. `fact_submit` returns `undefined_symbols` if you missed one. - **Cite every dependency by `fact_id`** — never "by the result above", never the problem statement as a math source. - **Every quantifier explicit; every introduced parameter (epsilon, k, …) carries an explicit range.** - **No handwave** ("obviously", "easy to see", "routine", "analogously", "by some classical argument") and **no chart-position references** ("as above"). - **Avoid duplicates.** `gm_search` the fact graph / global memory (or read `fact_graph/facts/`) for an existing fact with the same statement; if one exists, cite its `fact_id` instead of re-proving it. ## Submit and repair Call `fact_submit(statement, proof, predecessors=[...], glossary_introduces={...})`. Read the result: - `accepted: true, fact_id` — the fact is written. **Cite `fact_id`** downstream. - `accepted: false, repair_hints` (+ `undefined_symbols`) — revise: resolve critical errors first, then all remaining gaps; do not assume the fix is local — change strategy or backtrack if needed; then resubmit. Treat any `wrong` verdict, any critical error, or any gap as failure. - `verdict: "error"` — the verify service was unavailable; retry. - `accepted: true, write_error` (e.g. a predecessor was revoked) — the fact was not written; re-prove or avoid that predecessor. Every outcome is auto-logged to global memory (kind `verification`), so the feedback is shared — `gm_search` it to learn from others' rejections. ## The verifier is the only correctness authority If your own reasoning, the main agent's `master_guidance`, or any other LLM calls a result correct but `fact_submit` rejects it, the verifier wins. Always. Note the disagreement (a `dead_end` finding) and treat the "looks correct" opinion as the unreliable signal it was. A non-verifier opinion (including `master_guidance`) is for ideas and directions, never for correctness. ## Tools - `fact_submit` (the only path to verify a result and write a fact) - `gm_search` (check for an existing fact before submitting; read others' verification outcomes) - the fact graph is read directly (`fact_graph/facts/`, `glossary.json`)