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.