scottnarmstrong/leanautoformalizationskills/build-proof-dependency-graph

Build a Proof Dependency Graph

Construct the mathematical topology from the supplied proof text, after the author has approved a small set of exact one-declaration Lean anchor files. Produce a database that a later Lean orchestrator can use immediately, while making no claim that an anchor's proof has been completed.

Keep the boundary sharp

• Read the source corpus and its cited mathematical inputs. Among Lean files,

read only the designated frozen declaration files and frozen-anchor manifest needed to identify the author-approved anchors. Never read implementation modules, proof-status ledgers, or arbitrary Lean declarations.

• Do not interpret proof bodies, sorry, axioms, imports, or Lean status.

A manifest may allowlist draft sorry bodies, but that is later orchestration policy, not evidence this skill can use.

• Initialize Lean planning fields only:

LEAN_STATUS: NOT_STARTED, LEAN_REF: -, and LEAN_NOTE: - for ordinary nodes; use ASSUMED for explicit standing-assumption nodes and EXTERNAL for cited external results.

• Treat the bundled linter as a database and topology checker. It never

interprets Lean proof status and cannot decide whether the extracted mathematics is correct or complete.

• Treat FROZEN_ANCHORS as immutable Lean ABI nodes. Each anchor has one

manifest ID, declaration file, declaration export, source-record ID/version, and author-controlled elaborated ABI hash. With --source-root, the linter hashes the manifest file named in the graph header, parses its identity schema, and requires an exact unique match for every frozen graph node. It never reads Lean proof bodies or interprets manifest state, sorry, or proof metadata. A source-statement correction creates a new versioned anchor and invalidates old audits; neither graph edges nor amendments can change an anchor ABI.

• Record source-only statement fields for every node. For an anchor, they are a

review aid alongside its frozen Lean statement, not permission to edit it.

• The schema names CONTRACT_ID and CONTRACT_VERSION identify a

source-statement record only. That record is not a theorem statement, candidate declaration, approval surface, or substitute for the actual frozen Lean export.

• Stop after delivering the reviewed graph, coverage manifest, generated

dashboard, and unresolved source questions. Do not begin formalization.

Use the bundled resources

Before delegating, read references/agent-packets.md for the extraction and review packet specifications.

Copy these assets into the target project and replace their placeholders:

• assets/DEPGRAPH.template.md as the graph

database;

• assets/DEPGRAPH_COVERAGE.template.md

as the exhaustive source inventory.

Run scripts/proof_depgraph.py --help for linter options. Keep the script in the skill or copy it into the target project if the graph will be maintained there.

Phase 0: author-freeze anchors before graph extraction

Work source-first. Select one or a few declaration-sized definitions/theorems per subsection that carry its mathematical interface. Only their actual exact Lean declarations may become anchors. Markdown descriptions, candidates, tracked probes, placeholder types/bodies, fallback definitions, and promised future characterizations have no anchor status. A transient untracked file may elaborate the exact final command and must then be deleted.

The author approves the complete exact Lean command before dependency extraction. Place each in its own declaration-only .lean file. Freeze each approved keystone proposition or theorem with the exact body by sorry and manifest state DRAFT_SORRY; do not wait for its proof before anchoring the graph. The durable manifest must record and allowlist that exact body, provider, declaration/ABI hash, and quarantine. The theorem statement is already final but remains FROZEN_UNPROVED. Definitions neither contain nor depend on a draft placeholder.

If the source defines an object by a characteristic property, prove and audit its exact well-definedness theorem first. Only afterward materialize the definition and its separately named, sorry-free full characterization; treat them as one versioned semantic unit. Downstream graph nodes depend on the characterization theorem, not merely on the definition's codomain. The well-definedness theorem may itself be an exact frozen theorem root before the definition exists.

The well-definedness theorem must not assume any existence, integrability, linearity, quadraticity, symmetry, representability, or other proof step unless the source states it as a premise. Model those results as dependencies. After a genuine ∃! result is proved, unique choice is legitimate; a fallback or non-unique selection is not.

Create the manifest before the graph using the frozen-anchor manifest schema. For every anchor record its node ID, project-relative file, exact export, source-record ID/version, elaborated ABI SHA-256, source locator, author/version, and draft-body policy. The ABI hash is supplied and controlled by the authoring process; this skill records it but does not compute or certify it from Lean. With --source-root, the graph linter verifies the header's exact manifest file SHA-256 and binds graph fields to the JSON entry; it never opens Lean proof bodies.

Only then create the graph header: FROZEN_ANCHORS names these node IDs and FROZEN_MANIFEST records its durable relative path and hash. Every graph root must be an anchor. Non-anchor nodes must use - for all FROZEN_* fields. No anchor may be a route, step, application, assumption, or external node.

When the author splits one source theorem or lemma into multiple anchors, record the split ruling and its constant/witness policy in every affected source-statement record: shared means shared across exports; independent means each export may choose its own witness. A shared witness requires a joint frozen anchor; graph edges between separate existential exports do not make their witnesses equal. Do not derive either policy from graph topology.

Phase 1: freeze the extraction specification

Record before reading proofs:

1. the already author-approved root anchor or anchors;
2. every in-scope source file and a revision, hash, or dated snapshot;
3. the exact IDs and scopes of standing assumptions, recorded in

STANDING_ASSUMPTIONS, and the policy for cited external results;

1. stable notation, carrier, normalization, quantifier, and convention choices

that a global reviewer must track;

1. the threshold for a substantive proof-step node;
2. exclusions, such as background exposition outside the root closure;
3. the central writer's stable agent/session identity.

Prefer source labels as node IDs. For unlabeled Markdown results, derive IDs from stable heading anchors and semantic slugs. Use parent#slug for an unlabeled proof step. Never make a line number part of an ID; retain line numbers only as revisable locators.

Check every designated root anchor against its source statement before extracting its proof. Record all source-visible premises and the outer-to-inner quantifier order, especially dependency restrictions such as C depending only on d. The graph's source fields may not mention an intermediate estimate merely because the proof uses it, and they may never change the anchor file.

Phase 2: inventory before interpreting

Build the coverage manifest mechanically and then inspect it manually. Include:

• theorem-like environments and named claims;
• definitions used by proofs;
• labeled or reused displayed formulas;
• Markdown theorem/proof headings;
• explicit citations and cross-references;
• proof paragraphs likely to contain unnamed substantive steps.

Give every inventory item exactly one disposition: one or more graph nodes, or EXCLUDED with a concrete reason. An inventory is a checklist, not proof that coverage is complete; fresh reviewers must compare it with the raw corpus.

Phase 3: extract in parallel

Partition ownership into non-overlapping, line-addressable slices aligned to complete statement/proof units whenever possible. Read-only context may overlap across slice boundaries, but node ownership may not. Assign one worker per slice and keep one distinct orchestrator as the single writer and adjudicator. Choose models and reasoning effort appropriate to the mathematics and the repository's resource policy; give every worker a bounded brief.

Require workers to return packets only. Each proposed node must include:

• exact statement and proof locators;
• a stable source-family CONTRACT_ID and its CONTRACT_VERSION, which

together form the versioned source identity;

• normalized SOURCE_HYPOTHESES, SOURCE_QUANTIFIERS, SOURCE_CONCLUSION,

and CONSTANT_SCOPE fields read from the statement rather than its proof;

• a stable ID and kind;
• direct prerequisites with source evidence for every edge;
• explicit standing-assumption and external-input nodes;
• substantive child steps;
• alternative proof routes;
• ambiguities and cross-slice references.

Do not ask extraction workers to set Lean status or edit the database. Give them the approved anchor IDs and source statement locators, but do not give them implementation modules or proof-status material. Reuse a worker for follow-ups within its slice, but use fresh agents for independent review.

Phase 4: model the proof faithfully

Use only direct dependency edges. Do not add a prerequisite merely because it appears earlier in the paper. An edge can still be direct even when another path makes it transitively redundant: retain it when the target's own proof explicitly invokes or logically consumes that prerequisite.

Create a step node when omitting the step would hide a plausible Lean lemma or an independently failing obligation. Typical examples are a nontrivial estimate, construction, case split, parameter or witness choice, theorem application, quantifier closure, carrier change, or reused intermediate claim. Do not create nodes for routine algebra or purely syntactic rewrites unless they change hypotheses, constants, carriers, or quantifier strength.

If the source asserts or needs a substantive bridge without actually proving it, keep that bridge as a step or application node and mark NOTE with a clear SOURCE_GAP: explanation. Its STATEMENT_SOURCE may point to the target statement and its PROOF_SOURCE to the prose where the bridge is invoked. TOPOLOGY_STATUS judges whether this modeling is accurate, not whether the source proves the mathematics, so an independently confirmed gap can be REVIEWED. Do not silently fill an omitted bridge merely because a reviewer can reconstruct a proof; apply the substantive-step threshold to what the source actually supplies. Never invent a proof-status-like topology value.

Interpret DEPS conjunctively. If the source offers alternative derivations, create one KIND: route node for each derivation and list them in ROUTES on the target. One available route will later suffice. Never put alternatives in one comma-separated DEPS list. ROUTE_FOR is exclusively the ownership field for these route nodes; do not use it as a parent pointer for ordinary proof steps or displays.

Represent standing assumptions and external results as explicit leaf nodes. Do not hide them in notes or magic dependency tokens. Only IDs frozen in the header may use KIND: assumption; the linter rejects undeclared assumption nodes.