Generated from
folio-assistant-sci/skills/content/folio-paper-adapter/lean-formal-graph.md— do not edit here.
Lean formal dependency graph
The relation this skill owns
A block participates in two dependency relations. This skill owns the
formal one — what a proof actually invokes, machine-derived from
lean.ref. The editorial relation (uses[], what a reader must
have read) is owned by uses-editorial-review.
Never write formal dependencies into uses[]. They answer different
questions and diverge legitimately in both directions.
Where the formal edges come from. The graph reads
docs/audits/lean-atlas-deps.json, and each entry records its source. A
scan entry is a lexical guess (measured recall 0.63, folio-assistant#1492);
atlas and elaborated are elaborated and their type/value split can be
trusted. To produce elaborated edges, run the science layer’s extractor:
skill lean-formal-edges (folio-assistant-sci/skills/lean/), CLI
folio-assistant-sci/pipeline/formal-edges.ts, MCP tool
lean_formal_edges. It is tooling, so it lives there, not here.
Get a graph
# Does one exist yet?
bun run cat-harness-tools/pipeline/content-graph.ts content/<paper>
If it reports cache ABSENT — formal graph unavailable, populate it:
# Preferred: Lean Atlas (elaborated, authoritative)
cat-harness-tools/scripts/install-lean-atlas.sh # provisions the Lake require
lake exe atlas graph-data --output /tmp/atlas.json --pretty
# → adapt to folio's JSONL, then:
bun run cat-harness-tools/pipeline/lean-atlas-ingest.ts --ingest /tmp/deps.jsonl
# Fallback: no Lean toolchain needed
bun run cat-harness-tools/pipeline/lean-atlas-ingest.ts --scan content/<paper>
bun run cat-harness-tools/pipeline/lean-atlas-ingest.ts --stale
Know which source you have — it changes what you may claim
formalSource | What it is | What you may conclude |
|---|---|---|
atlas | Elaborated. Real type/value split. | Authoritative |
scan | Syntactic. Misses simp/instance/unfolding deps; can over-report a coincidental name. | Indicative — a missed edge SHRINKS results, which is the dangerous direction |
| absent | No graph | n/a. Not “no dependencies” |
The last row is the one agents get wrong. An empty formal edge set means the data was unavailable, not that the corpus has no formal structure. Say which you have.
Type vs value edges
- type — the declaration’s signature mentions the target. Changing the target changes what this block claims.
- value — only the proof term mentions it. Changing the target changes how the block is justified, not what it says.
That split is why a proof-body rewrite no longer invalidates
statement-level QA (lean_granularity: "statement"), and why the
semantic cone propagates over type edges only.
What to use it for
| Question | How |
|---|---|
| What breaks if this changes? | g.cone(label) — the union, the default |
| What must a reader read first? | g.cone(label, "editorial") — a different question |
| Is the narrative leaving a gap? | uses-formal-coverage (advisory; most formal-only edges are correct) |
| Who owns this declaration? | g.declOwners / lean-ref-owns-decl |
| What should I review first? | semantic-review-scoping |
| Does a proof use the lemmas it was planned to use? | compare the block’s planned predecessors with its value edges. A proof that uses none of them is a reason to re-read the statement — a proof easier than the intended mathematics is evidence about the statement. Advisory; see blueprint-driven-formalization §4 |
Declaration ownership
A declaration can be attached to only one block. When two claim it, the loser silently forfeits its formal edges.
lean-ref-owns-decl audits this, and deliberately does not flag a
prop:x + prf:x pair sharing a decl — that is legitimate and common.
Only two statement-bearing blocks colliding is a defect. In practice
those are copy-paste errors, and they are worth fixing on sight: a real
corpus had a “Unital subset” definition pointing at a Gröbner-basis
declaration.
Interaction with other skills
| Skill | Interaction |
|---|---|
uses-editorial-review | Owns the editorial relation; consumes the advisory coverage signal |
semantic-review-scoping | Consumes type edges to bound agent review |
detangler-integration-watcher | Editorial-only by design — do not feed it formal edges |
critical-path-analysis | Uses the union; impact is a union question |
lean-cache-restore | Restore oleans before any Lean work |