| name | verify-proof |
| description | 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. |
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)
