From theorem target to compiled certificate

The ABRL proof workflow

Automation proposes and attempts proof leaves, but target fidelity, explicit assumptions, local compilation, and reviewer gates determine whether a result is achieved.

The repository contract

literature theorem or new bandit/RL target
→ theorem card and assumption ledger
→ exact Lean statement and proof-DAG leaves
→ compiled Lean certificate
→ synchronized explanation and implementation map
→ reusable retrieval memory

A theorem card is evidence for a route. It is never displayed as a local proof unless the corresponding declaration is imported or proved and the Lean gate succeeds.

Adaptive orchestration, one evidence standard

A hybrid candidate—not a measured winner

The scheduler can run the established hierarchical director–planner–worker loop or a bounded master–worker trial in which several workers explore independent proof routes. Both receive the same frozen target, ordered route packet, budget, source packet, and deterministic gates; the route-packet hash makes that equality checkable.

Current decision. The structured log ledger does not yet justify declaring either harness universally better, so the hierarchical loop remains the default. The master–worker route is experimental and is enabled only when parallel alternatives are genuinely independent. A trial wins only by delivering a stronger checked certificate, a smaller named blocker, or a reusable lemma—not by producing more messages or attempts.

Target governor

Hierarchy owns the theorem

One authority freezes the statement, assumptions, source interpretation, proof frontier, and acceptance contract.

Bounded exploration

Workers own disjoint proof leaves

Parallelism starts only after routes have distinct fingerprints, explicit deliverables, and non-overlapping files.

Independent synthesis

Reviewer owns promotion

The master may summarize results, but it cannot repair evidence labels or bypass Lean and target-fidelity review.

Design hypothesis. Hierarchical control is most useful for target fidelity and ambiguous interfaces; bounded parallel workers are most useful after the proof DAG exposes independent mathematical leaves. This hypothesis is what the matched experiment must test.

flowchart TB
    Target["Frozen theorem target<br/>assumptions + source packet + budget"] --> Governor["Hierarchical target governor<br/>owns statement + proof frontier"]
    Governor --> Split{"Are the next proof leaves<br/>mathematically independent?"}
    Split -->|no or unclear| H["Single routed worker<br/>diagnose one interface"]
    Split -. "yes, in matched trials" .-> P["Bounded parallel worker pool<br/>disjoint routes + disjoint files"]
    H --> Synthesis["Evidence-only synthesis<br/>certificate · blocker · reuse · cost"]
    P --> Synthesis
    Synthesis --> Review["Independent reviewer<br/>target fidelity + evidence audit"]
    Review --> Gate{"Deterministic gate<br/>focused compile + repository check"}
    Gate -->|accepted| Library["BanditRLlib declaration<br/>and synchronized explanation"]
    Gate -->|diagnostic| Log["Matched trial log<br/>certificate · blocker · reuse · cost"]
    Log --> Governor
    Library --> Memory["Reviewer-gated retrieval memory"]

Evidence-aware scheduler comparing a hierarchical loop and a bounded master-worker trial before a common Lean and reviewer gate · editable Mermaid source

Generated from structured run logs

Current harness-comparison evidence

The table reports only lower/worker executions that share one frozen target and one hashed route packet, then receive a separate reviewer-owned verdict. Historical activity without that comparison contract is excluded.

Prototype

Decision statusInsufficient Evidence

Matched evidence0 of 2 required

Recommended defaultretain-current-default

Next matched armhierarchical

Observed log coverage

hierarchical

0 observed attempts

0 reviewer-joined · 0 unreviewed · 0 experiment ids. These counts describe the log, not a causal comparison.

master-worker

1 observed attempt

0 reviewer-joined · 1 unreviewed · 1 experiment id. These counts describe the log, not a causal comparison.

Why 1 observed experiment cannot enter the matched table

sgb-t2-round33-master-worker: both harness arms are not present

Every valid pair needs both execution arms, the same frozen target and route-packet hash, plus a separate reviewer verdict for each attempt. An unreviewed worker claim stays visible here but contributes zero substantive score.

Deterministic matcherActive

Keep only equal-target, equal-route-packet trials with reviewer-owned outcomes and verifier evidence.

Bounded GPT reviewAwaiting matched evidence

The review packet can explain bottlenecks, duplication, and context cost; it cannot relabel an attempt or invent a winner.

Promotion gateDefault retained

A default changes only after enough matched experiments and the same independent Lean-and-target review.

Harness	Runs	Attempts	Reviewed	Substantive	Score	Critical seconds
hierarchical	0	0	0	0	0	0.0
master-worker	0	0	0	0	0	0.0

Why no winner is shown. need at least 2 matched experiments; found 0 When executed, the bounded GPT-review stage receives this deterministic report and may interpret bottlenecks or propose the next matched experiment, but it cannot promote unreviewed output or override this evidence boundary.

Generated attempt graph

What the harness has actually tried

The graph below is regenerated by harness-compare from eligible structured rows. It is intentionally sparse while the ledger contains no matched trials; future reviewer-validated attempts will appear as nodes rather than being summarized from memory.

flowchart TD
  ROOT["Frozen theorem target"]
  H["Hierarchical: upper → middle → lower → reviewer"]
  M["Master–worker: master → parallel workers → synthesis → reviewer"]
  ROOT --> H
  ROOT --> M
  A0_sgb_t2_round33_worker_consumer["sgb-t2-round33-worker-consumer\nunreviewed · reported compiled-leaf/compiled"]
  M --> A0_sgb_t2_round33_worker_consumer
  class A0_sgb_t2_round33_worker_consumer unreviewed
  classDef substantive fill:#dff5e7,stroke:#176b3a,color:#123b25
  classDef failed fill:#fde7e7,stroke:#a33a3a,color:#5f1d1d
  classDef unreviewed fill:#f4f1e8,stroke:#8c8268,color:#3f3a2f

Attempt graph generated from the structured harness ledger; an unpaired arm means that no matched experiment has entered the comparison table · generated Mermaid source

Open the deterministic JSON Open the GPT review packet Read the comparison method

Model-assisted interpretation · hash-bound to the ledger above

GPT diagnosis and candidate internal harness

GPT read the deterministic metrics and eligible recent rows, then returned one machine-checked advisory plus an editable architecture diagram. It cannot validate attempts, change evidence labels, or select a winner against the deterministic gate.

Advisory

Suggested defaultretain-current-default

Confidencelow

Evidence gateInsufficient Evidence

Adoption statusHypothesis only · not adopted

What the log supports

Deterministic decision status is insufficient-evidence.
Minimum matched experiments required is 2; found 0.
Matched evidence reports zero experiments, attempts, reviewed attempts, obligations closed, declarations, and substantive score for both harnesses.
One unmatched master-worker run reports a compiled leaf with four new declarations and reused declarations, but it is excluded because the paired hierarchical arm and reviewer-owned verdict are absent.

Risks and unknowns

Adopting master-worker now would overfit to an unmatched, unreviewed success signal.
Adopting hierarchical as empirically superior would also be unsupported because it has no matched execution.
A hybrid can create a master bottleneck unless synthesis stays narrow and reviewer gating remains independent.

Candidate change

No scheduler default change. Test a light planner, bounded disjoint workers, evidence-only synthesis, and an independent reviewer as the master-worker arm of the next matched experiment.

Next matched experiment

Target: PAPER-AUDIT-NEURIPS-2025-SGB-PHASE-TRANSITION-PROSPECTIVE
Route Packet: Use the same frozen route packet for both arms.
Arms: hierarchical
master-worker
Matching Requirements: same experiment id
same target fingerprint
same frozen route-packet hash
separate reviewer-owned verdict for each execution attempt
Primary Metric: reviewer-validated substantive mathematical progress

flowchart TD
    A["Frozen target + route packet"] --> B["Light planner"]
    B --> C1["Worker: route A"]
    B --> C2["Worker: route B"]
    B --> C3["Worker: route C"]
    C1 --> D["Evidence-only synthesis"]
    C2 --> D
    C3 --> D
    D --> E["Independent reviewer gate"]
    E --> F{"Lean + target fidelity"}
    F -->|accepted| G["Record validated progress"]
    F -->|rejected| H["Record diagnostics only"]

GPT-proposed internal harness for the next matched experiment; the diagram is advisory and does not report a measured winner · model-proposed Mermaid source

Interpretation boundary. This advisory is bound to latest.json by SHA-256. With 0 valid matched experiments, it retains the current default and proposes only what to test next.

Open GPT review Open parsed advisory JSON Open candidate architecture

Machine-auditable longitudinal evidence

One frozen target, seven interface closures

This route trace asks whether the first unresolved source-shaped interface moved while the mathematical target stayed fixed. It does not compare schedulers or measure speed.

Partial

Recorded states8

Ordered closures7

Separate fences6 of 7

Theorem 2 terminalOpen

The seven-field target projection keeps SHA-256 26833d037458820f… across 8 freeze-record revisions. The frontier moves from SGB-T2-NATIVE-PREFIX-IDENTIFICATION to SGB-T2-APPENDIX-C-PHASE-TRIGGER; Theorem 2 remains open.

Inspect all seven dependency-ordered closures

SGB-T2-NATIVE-PREFIX-IDENTIFICATIONBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_map_frestrictLe_eq_native closes the interface; next: SGB-T2-NATIVE-FULL-LAW-TRANSPORT. Evidence: index + typed canary; no separate fence.
SGB-T2-NATIVE-FULL-LAW-TRANSPORTBanditRLProof.Thompson.latentArmStreamVisibleTrajectoryMeasure_eq_native closes the interface; next: SGB-T2-SELECTED-BLOCK-TRANSPORT. Evidence: statement fence recorded.
SGB-T2-SELECTED-BLOCK-TRANSPORTBanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_map_optimalPullTimeRewardBlock_eq_latentMasked closes the interface; next: SGB-T2-PHASE-EVENT-TRANSPORT. Evidence: statement fence recorded.
SGB-T2-PHASE-EVENT-TRANSPORTBanditRLProof.StochasticGradientBandit.twoArmFixedIIDTrajectoryMeasure_appendixCGeneratedPhaseEvent_eq_latent closes the interface; next: SGB-T2-PHASE-DICHOTOMY. Evidence: statement fence recorded.
SGB-T2-PHASE-DICHOTOMYBanditRLProof.StochasticGradientBandit.twoArmAppendixCRewardPhaseProbability_eq_generated_add_missing closes the interface; next: SGB-T2-MISSING-PULL-STARVATION-BRIDGE. Evidence: statement fence recorded.
SGB-T2-MISSING-PULL-STARVATION-BRIDGEBanditRLProof.StochasticGradientBandit.twoArmAppendixCMissingPullLatentPhaseEvent_subset_terminalCountBelow closes the interface; next: SGB-T2-MISSING-PULL-REGRET-CONSUMER. Evidence: statement fence recorded.
SGB-T2-MISSING-PULL-REGRET-CONSUMERBanditRLProof.StochasticGradientBandit.twoArmFixedIIDMissingPullLatentPhase_charge_mul_probability_le_integral closes the interface; next: SGB-T2-APPENDIX-C-PHASE-TRIGGER. Evidence: statement fence recorded.

Interpretation boundary. This is one post-hoc route trace. It is evidence that named dependencies closed without changing the frozen target projection; it is not evidence of harness superiority, proof-search acceleration, or a causal effect.

Open deterministic JSON Open compact CSV

Reproducible gates

For a real A/B pilot, create both arms from the same route file, experiment id, and target fingerprint. The hierarchical arm executes the packets sequentially; the master–worker arm executes the same packets concurrently.

python3 tools/bandit.py run-cycle <task-id> --harness hierarchical --experiment-id AB-001 --target-fingerprint <sha256> --lower-count 2 --parallel-route-json routes.json
python3 tools/bandit.py run-cycle <task-id> --harness master-worker --experiment-id AB-001 --target-fingerprint <sha256> --lower-count 2 --parallel-route-json routes.json
python3 tools/bandit.py blueprint-refresh <task-id>
python3 tools/bandit.py harness-compare --task <task-id>
python3 tools/bandit.py reference-index
python3 tools/bandit.py unfinished
python3 tools/bandit.py check
python3 website/scripts/build_site.py --lean-verified
python3 website/scripts/check_site.py
python3 website/scripts/ide_server.py

The website build scans Lean source directly, including declarations whose keyword and name span separate lines. A new declaration therefore enters the catalog without a hand-edited index; major results still need a reviewed teaching note and milestone entry. The IDE server is a separate loopback-only development command and is never part of the public Pages deployment.

Failure is recorded, not hidden

If a proof attempt repeatedly fails, audit the statement, hypotheses, and possible counterexamples before broad tactic search.
If a route lacks a trajectory law, measurability proof, or integrability contract, name that interface as the blocker.
If prose is stronger than Lean, weaken the prose or add the missing theorem; never promote a plan to compiled status.
If a general lemma belongs in Mathlib, keep the project wrapper thin and record the candidate route.