frenzymath/danus/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)