Proof Orchestrator

Proof Orchestrator

Role

Run proof work across three interfaces:

1. Internal: Codex owns the local search, falsification, correctness audit, notation audit, exposition, and run record. Complete every concrete local next action that remains justified and feasible.
2. External: When the internal search is operationally exhausted, package the verified setting, attempted routes, strongest partial results, and smallest unresolved blocker for an external solver. No provider is the default.
3. User: Keep the user informed at meaningful decision points and preserve their authority over theorem changes, source disclosure, provider choice, uploads, browser operation, and paid calls.

External help follows the Internal Exhaustion Gate below, unless the user explicitly requests earlier consultation. In either case, first prepare an audit-ready local account of what is known and what remains unresolved.

For GPT Pro, Claude/Fable, or any other external solver, use an available authorized adapter or give the user a manual handoff. If the user selects GPT Pro and asks Codex to perform the call, load call-gpt-pro.

Run Directory And Canonical Record

Keep each run under:

mindflows/<YYMMDDHH-num>/

Use only the files needed by the run:

task.md              # precise theorem or proof obligation
materials.md         # definitions, givens, notation, and source excerpts
local-proof.md       # Codex's proof attempt or isolated blocker
approach-registry.md # optional route portfolio for difficult proof searches
sources/             # stable local source snapshots
source-manifest.md   # source role, disclosure status, and external filename
external-brief.md    # provider-neutral problem and evidence package
provider-prompt.md   # optional provider/interface-specific rendering
handoff.md           # chosen route, authority, transfer order, and status
external-output.md   # returned answer, kept as raw evidence
audit.md             # correctness and source-alignment audit
final.md             # verified, simplified, user-facing proof
codex-ledger.md      # run state and provenance, optional
next.md              # next narrow obligation, optional

Use only the files the run needs. external-brief.md is the canonical, provider-neutral handoff. Create provider-prompt.md only when a selected provider or interface requires a distinct rendering.

Do not create provider-specific prompts, handoff.md, or remote project state before the local attempt unless the user explicitly requests an external handoff. Preparing a local external-brief.md after the Internal Exhaustion Gate passes does not itself authorize external contact.

Continuing a Project

Treat an existing run, next*.md, redo*.md, or continuation artifact as a project continuation. First read any prior next/redo/continuation files that exist. Treat completed run artifacts and prior external conversations as append-only evidence; do not overwrite them.

Always create a new run directory for new proof work. Record the prior run ID, the exact files read, inherited proved/conjectural/rejected claims, preserved sources, and the single current obligation.

When inheriting an approach registry, preserve family identities and blocker-strength classifications. Keep a blocked route blocked unless the new run records a valid novelty key under references/portfolio-search.md.

If a continuation reaches external consultation, prepare a new external-brief.md for the current obligation. Reuse prior sources only after checking that they still match the frozen target. Prefer a fresh external conversation unless handoff.md explains why prior context is required.

Status Labels

Use these labels in codex-ledger.md, audit.md, or handoff.md:

• INTERNAL_ATTEMPT
• INTERNAL_PROVED
• INTERNAL_EXHAUSTED
• INTERNAL_STOPPED_WITH_ACTIONS_REMAINING
• ASK_USER
• READY_FOR_EXTERNAL_BRIEF
• READY_FOR_MANUAL_HANDOFF
• READY_FOR_AUTHORIZED_DISPATCH
• WAITING_FOR_EXTERNAL_OUTPUT
• EXTERNAL_OUTPUT_RECEIVED
• NEEDS_EXTERNAL_FOLLOWUP
• AUDIT_FAILED
• READY_FOR_USER

Notation Gate

When the user asks about notation or symbols, when the proof is theorem-heavy, or when one proof step contains at least five nonstandard symbols, read references/notation-audit.md and include this exact scorecard in audit.md or the user-facing audit:

Core semantic objects retained: <retained>/<declared> (<percent>)
Undefined symbols: <count>
Symbol collisions: <count>
One-use definitions: <count>/<all new symbols> (<percent>)
Maximum parallel representations of one object: <count>
Maximum alias-chain depth: <count>
Maximum active nonstandard symbols in one proof step: <count>

Do not rename, merge, omit, or replace these lines with other useful findings. Report logical gaps, domain errors, and irrelevant notation after the fixed scorecard. Core-object retention must be 100%, and undefined symbols and collisions must both be zero before READY_FOR_USER.

Never improve the scorecard by inventing a definition, domain, assumption, identity, or relation that the source does not supply. If an undefined symbol or missing implication cannot be resolved from authoritative material, keep it in the audit, mark the proof AUDIT_FAILED or ASK_USER, and rewrite only the valid fragment or the diagnosis.

Derivation Structure Gate

For every nontrivial derivation, organize the user-facing proof from the target downward, even if the proof was discovered bottom-up:

1. State the target and its role: "To prove A, it is enough to establish B, C, and D," together with the lemma, identity, or inference that makes those subgoals sufficient.
2. Derive each immediate subgoal and state where it comes from: an assumption, definition, prior lemma, or an explicitly shown calculation.
3. If a subgoal has its own dependencies, expand it in the same target-first form. Order dependent subgoals by their true dependency relation rather than presenting a misleading flat list.
4. Recombine the established subgoals and explicitly return to the original target.

This is an exposition rule, not a license to reverse an implication or hide a gap. Check that the dependency graph is acyclic, every reduction is justified, and no subgoal silently assumes the target. Do not force this scaffold onto a one-step argument where it would add more ceremony than clarity.

Record Top-down derivation structure: PASS, FAIL, or NOT_APPLICABLE in audit.md. A nontrivial derivation cannot be READY_FOR_USER while this gate is FAIL.

Search Portfolio Gate

For a research-level, open-ended, or repeatedly stalled obligation, read references/portfolio-search.md before committing to one proof route. Create approach-registry.md, compare routes by their mathematical mechanism, classify the strength of every central blocker, and run task-specific adversarial checks. For a routine proof with a direct path, skip this gate and do not create the registry.

An expected answer is a search direction, not a proof premise. Do not assume a theorem is true merely because the user, benchmark, or prior model output says a proof exists. Use independent workers only when they are explicitly authorized and available; the gate must also work as a sequential local search.

Three-Interface Contract

Internal Interface

The local run is the canonical source of truth. Follow the Search Portfolio and Internal Exhaustion Gates where applicable, record both positive and negative evidence, and perform Codex's own correctness audit. A second model never substitutes for that audit.

External Interface

External interaction begins from the provider-neutral external-brief.md specified in the External Handoff Contract. Choose a provider only after the mathematical role is clear. The provider may be GPT Pro, Claude/Fable, another model, a human expert, a theorem prover, or a specialized service. Record the choice and reason in handoff.md. Provider- specific connection instructions belong in the selected adapter or provider-prompt.md; they must not determine the core proof workflow.

User Interface

Report ambiguity, missing information, a genuine blocker, justified external help, and the audited external result. Ask before changing the theorem, disclosing non-approved material, choosing materially different external routes, operating a browser, uploading files, sending messages, or spending credit. If user information is the blocker, mark ASK_USER. Before external contact, provide the decision record required in workflow step 6.

Internal Exhaustion Gate

INTERNAL_EXHAUSTED means operationally exhausted under the frozen target, available local tools and sources, and any explicit user budget. It does not claim that no proof exists or that all mathematics has been searched.

The gate passes only when all of the following are recorded in audit.md or codex-ledger.md:

1. The exact target, assumptions, quantifiers, conventions, and allowed sources are frozen; missing user choices or sources have been separated from proof difficulty.
2. Codex attempted the actual completion task and audited every claimed result, rather than stopping after a difficulty probe or delegating the original theorem unchanged.
3. For a routine task, the direct route and its natural repairs were completed, rejected, or reduced to an exact blocker. For a research-level, open-ended, or repeatedly stalled task, the Search Portfolio Gate was applied.
4. Every approach family is CANDIDATE, BLOCKED, or REJECTED; each blocked family has a smallest blocker, blocker-strength classification, and attempted falsification. No family remains merely EXPLORING.
5. No concrete local next action remains that is both relevant and feasible. Unused actionable ideas, unchecked hypotheses, or unrun decisive checks mean the gate fails.
6. The strongest locally proved result, the exact residual obligation, and Equivalent-strength blocker: <YES|NO|UNKNOWN> are recorded.
7. The reason for stopping is epistemic rather than cosmetic: additional local work would require a new mechanism, a missing authoritative source, a user decision, unavailable capability, or effort beyond an explicit budget.

If work stops because of a user or environment budget while concrete actions remain, use INTERNAL_STOPPED_WITH_ACTIONS_REMAINING, list those actions, and do not claim exhaustion. External consultation may still be offered if the user requests it, but the handoff must disclose that local search was truncated.

If the user explicitly requests external consultation before this gate passes, honor the request within its authorization boundary, but mark the exception in handoff.md and include the untried local actions in external-brief.md.

Workflow

Default route: freeze target -> maintain evidence -> exhaust actionable internal work -> local correctness audit -> exposition edit -> final. When the Internal Exhaustion Gate passes: prepare a provider-neutral external brief -> report the decision record to the user -> use the user-selected manual or authorized route -> ingest raw output -> return to internal proof and audit -> final.

1. Freeze the target.
   • Decide whether the request is new or a continuation.
   • State the exact theorem, assumptions, quantifiers, and allowed sources.
   • Do not broaden or repair the theorem silently.
2. Maintain local evidence.
   • Read only the files needed to understand the target.
   • Copy stable, directly relevant snapshots into sources/ when the original may change or cannot be referred to reliably.
   • Keep private run materials in the run directory, never in the skill package.
3. Run the internal proof search.
   • Try to complete the actual proof, disproof, counterexample, or diagnosis; do not stop at a difficulty probe.
   • Check definitions, boundary cases, domains, support, topology, quantifiers, and imported theorem hypotheses.
   • Write local-proof.md with the conclusion, proof attempt, dependencies, and any unresolved gap.
   • Apply the Search Portfolio Gate when it applies, and continue while a relevant, feasible concrete next action remains.
4. Audit and classify the internal result.
   • Verify every theorem, lemma, reduction, equality, bound, constant, and quantifier against the stated assumptions and local sources.
   • Distinguish proved, imported, conjectural, repaired, and unsupported statements.
   • For an unresolved run, record Equivalent-strength blocker: YES, NO, or UNKNOWN in audit.md or codex-ledger.md and justify the classification.
   • If the exact target passes audit, mark INTERNAL_PROVED and continue to exposition.
   • If information or a theorem choice is missing, mark ASK_USER and present the smallest question that changes the proof state.
   • Otherwise apply the Internal Exhaustion Gate and use its status rules. If it does not pass, return to step 3. Optional external review remains additional evidence, not a substitute for Codex's audit.
5. Edit the proof for exposition.
   • Apply the Notation and Derivation Structure Gates when they apply.
   • Lead with the conclusion, preserve each core semantic object, and retain every non-obvious logical dependency.
   • Prefer a short direct argument to decorative formalism; do not polish an unresolved gap into an apparently complete proof.
6. Prepare the external brief only when justified.
   • Proceed only under the condition and exception rules in the Internal Exhaustion Gate.
   • Complete the External Handoff Contract below and mark READY_FOR_EXTERNAL_BRIEF.
   • Before contact, present what is proved locally, what was tried, what remains, why further local work is not actionable, what would be shared, and the available manual or authorized-dispatch routes. If a consequential choice remains open, mark ASK_USER while retaining the readiness event.
7. Select and authorize the external route.
   • Record the route and authority in handoff.md as required by the External Handoff Contract.
   • For a manual route, provide transfer instructions and mark READY_FOR_MANUAL_HANDOFF; after transfer, mark WAITING_FOR_EXTERNAL_OUTPUT.
   • For Codex-operated dispatch, require explicit current authority, mark READY_FOR_AUTHORIZED_DISPATCH, and load the relevant adapter skill. After sending, mark WAITING_FOR_EXTERNAL_OUTPUT.
8. Ingest the returned material as evidence.
   • Save user-pasted or Codex-retrieved text as external-output.md or the provider-specific filename recorded in handoff.md.
   • Mark EXTERNAL_OUTPUT_RECEIVED and apply only the formatting repairs allowed below before mathematical auditing.
   • Record the provider, conversation or task identifier when available, files actually disclosed, prompt actually sent, and whether the response is complete.
9. Re-enter the internal loop.
   • Audit every external claim against the frozen target and authoritative sources; use only valid ideas as new local proof actions.
   • If the target passes, return to step 5; final.md may be clearer than the raw answer but must preserve necessary logic and epistemic labels. If a gap remains, first pursue the new local actions it creates; mark NEEDS_EXTERNAL_FOLLOWUP only after isolating the residual blocker and recording the applicable exhaustion or early-consultation exception.

External Handoff Contract

1. Keep authoritative copies under sources/ with stable generic filenames.
2. Write source-manifest.md with, for each source:
   • local relative path;
   • external-visible filename;
   • why it is needed and whether it is authoritative or contextual;
   • whether it must be transferred separately or is faithfully summarized in materials.md;
   • disclosure status: approved, not-approved, needs-user-approval, or not-needed;
   • readiness status: ready, missing, optional, or returned-by-user.
3. Make external-brief.md self-contained and provider-neutral. Include, in this order:
   • exact target, assumptions, quantifiers, object conventions, and allowed sources;
   • definitions and source filenames the solver will see;
   • locally verified results and their dependencies;
   • attempted approach families, concrete failures, counterexamples, and blocker strengths;
   • the smallest unresolved blocker and its relation to the original target;
   • any concrete local actions left untried because the user requested early consultation or a budget stopped the run;
   • exact requested output, permitted theorem imports, verification expectations, and a completion marker such as END_EXTERNAL_OUTPUT.
4. If a provider or interface needs special formatting, derive provider-prompt.md from external-brief.md. Do not weaken assumptions, omit failed routes that prevent repetition, or promote conjectures to facts. Keep connection mechanics out of the canonical brief.
5. Make handoff.md record the selected solver and rationale, authority granted, approved disclosures, files and prompt actually sent, transfer order, return path, status, and any deviation from the canonical brief.

If a required source or disclosure decision is missing, mark ASK_USER or the handoff blocked rather than silently replacing it with memory. A narrow blocker is the default request. Ask for the full theorem only when independent search or whole-proof verification is the explicit external role, and say why that wider scope is useful.

External Output Preservation And Repair

Keep external-output.md or the recorded provider-specific output file recognizable as raw external evidence. Formatting repair may fix copy corruption but must not change claims, constants, assumptions, theorem status, or proof order.

Required checks:

• Confirm the requested completion marker is present.
• Balance display-math delimiters and inspect suspicious blank lines.
• Repair obvious escaped-brace corruption such as \left{ to \left\{ and \right} to \right\} only when the intended delimiter is unambiguous.
• Remove residual interface or copy separators only when their intended role is clear; otherwise flag them in audit.md.
• Scan for malformed operators, stray Markdown markers, and broken right delimiters.

Record nontrivial repairs in audit.md or codex-ledger.md. Perform substantive clarity and notation editing in final.md, after the correctness audit, rather than rewriting the raw output.

Guardrails

• Never invent missing citations, source statements, assumptions, or proof steps to avoid a blocker or make a handoff look complete.
• Never treat invoking this skill as authority for browser control, uploads, remote messages, API spending, provider selection, or another external turn.
• Never disclose a source marked not-approved or needs-user-approval.
• Do not reuse prior authorization, silently switch providers, or infer a paid/API fallback after another route fails.
• Do not present a comparable, equivalent, or stronger missing lemma as routine progress. Reopen a blocked route only when references/portfolio-search.md supplies a valid novelty key.
• Audit before simplifying. Preserve any step whose removal would make a non-obvious inference unverifiable.
• Treat an external answer as raw evidence. Re-enter local search and audit before accepting it, pursue any new local actions before requesting a follow-up, and obtain new authorization before every dispatch.
• If correctness and elegance conflict, preserve correctness and state the remaining exposition issue explicitly.