ASTIS Automation Workflow

Source-backed leaves, independent review, Lean certificates.

The hierarchical loop coordinates mathematical source audit and Lean implementation. It does not convert an agent report, task card, or theorem-shaped data record into a proof.

System architecture

Four proving layers feed reusable formal memory

ASTIS hierarchy and Samplinglib formal memory — Typed artifacts cross every layer; accepted certificates enter Samplinglib, while unresolved leaves return to planning.

Agent execution detail

flowchart LR
  Human["Human objective<br/>faithful textbook route"]:::human
  UpperMath["upper_source_math<br/>source + hidden hypotheses"]:::upper
  UpperDag["upper_proof_dag<br/>shared roots + active leaf"]:::upper
  MiddleSource["middle_source_correspondence<br/>exact theorem boundary"]:::middle
  MiddleLemma["middle_technical_lemma<br/>ASTIS / Mathlib search"]:::middle
  LowerProof["lower_2<br/>one Lean declaration"]:::lower
  LowerScout["lower_1 + lower_3<br/>proof/API packets"]:::lower
  Gate["reviewer_gate<br/>Lean + source + fake-closure gate"]:::review
  Waste["reviewer_waste<br/>duplicate/churn audit"]:::review
  Blue["compiled local leaf<br/>Registry + module inventory"]:::compiled
  Obligation["typed proof obligation<br/>smaller blocker"]:::blocked

  Human --> UpperMath
  Human --> UpperDag
  UpperMath --> MiddleSource
  UpperDag --> MiddleLemma
  MiddleSource --> LowerProof
  MiddleLemma --> LowerProof
  MiddleLemma --> LowerScout
  LowerScout --> LowerProof
  LowerProof --> Gate
  LowerProof --> Waste
  Gate -->|accept| Blue
  Gate -->|narrow| Obligation
  Obligation --> UpperMath

  classDef human fill:#172033,stroke:#172033,color:#ffffff,stroke-width:2px;
  classDef upper fill:#ece6ff,stroke:#6938ef,color:#172033,stroke-width:1.5px;
  classDef middle fill:#dcecff,stroke:#155eef,color:#172033,stroke-width:1.5px;
  classDef lower fill:#dcfae6,stroke:#087443,color:#172033,stroke-width:1.5px;
  classDef review fill:#fff2c7,stroke:#9a6700,color:#172033,stroke-width:1.5px;
  classDef compiled fill:#dcecff,stroke:#155eef,color:#172033,stroke-width:2px;
  classDef blocked fill:#ffe5e5,stroke:#c92a2a,color:#172033,stroke-width:2px;

The concrete upper, middle, lower, and reviewer responsibilities from the current harness.

Upper

Audits the source theorem and shared-root DAG, selects one active leaf, and retires stale routes.

Middle

Searches existing ASTIS/Mathlib interfaces, fixes the exact theorem boundary, and writes a lower-ready packet.

Lower

Implements one declaration or returns one strictly smaller source-cited proof obligation with typed failure feedback.

Reviewer

Runs deterministic gates, checks hidden hypotheses and source correspondence, and rejects wrapper churn or fake closure.

Reproducible gate

python3 tools/astis.py check

Lean gate passed for this exact Lean source digest.

Failure is retained

Missing assumptions become explicit proof obligations.
API mismatches are recorded with the attempted declaration and error class.
External theorems remain upstream dependencies until ported and compiled locally.
Repeated same-shape failures trigger statement review rather than silent theorem drift.

Paper-to-proof-leaf conversion

flowchart LR
  S["Chewi source anchor<br/>chapter · section · page · equation"] --> E["ASTIS faithful exposition"]
  E --> R["Rigorous detail packet"]
  R --> D["Lean declaration"]
  D --> F["Lean source file"]
  D --> T["Tests / build gate"]
  D --> G["Registry entry"]
  G --> P["Generated site status"]
  T --> P

The textbook statement is decomposed through assumptions and shared roots before lower proof work begins.