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.

Hierarchical loop

sequenceDiagram
  participant U as Upper director
  participant M as Middle planner
  participant L as Lean worker
  participant R as Reviewer
  participant G as Deterministic gate

  U->>M: Select one theorem route and preserve the target
  M->>M: Search Mathlib, local declarations, and theorem cards
  M->>L: Issue one exact leaf with hypotheses and failure policy
  L->>G: Compile focused module and Tests.Basic
  G-->>L: Errors or compiled certificate
  L->>M: Proof term or precise blocker
  M->>R: Synchronized Lean, prose, route, and memory
  R->>G: Run tools/bandit.py check
  G-->>R: Repository-wide verdict
  R-->>U: Accept, refine, or reopen the statement audit

Upper, middle, Lean worker, reviewer, and deterministic-gate sequence · editable Mermaid source

Reproducible gates

python3 tools/bandit.py blueprint-refresh <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.