# Plan Graph

> Read, edit, and SEMANTICALLY SEARCH the formalization statement plan stored in the Mem0-g plan graph (the replacement for statements.json). Use whenever you need to inspect, query, or modify statements, dependencies, status, or informal notes; run the Lean dependency sync; or find statements/notes by MEANING (LeanSearch-v2-style two-stage retrieval: OpenAI embedding recall → LLM rerank) — e.g. to…

- **Type:** Skill
- **Install:** `agentstack add skill-merleanprover-merlean-plan-graph`
- **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior
- **Seller:** [MerLeanProver](https://agentstack.voostack.com/s/merleanprover)
- **Installs:** 0
- **Category:** [AI & ML](https://agentstack.voostack.com/c/ai-and-ml)
- **Latest version:** 0.1.0
- **License:** Apache-2.0
- **Upstream author:** [MerLeanProver](https://github.com/MerLeanProver)
- **Source:** https://github.com/MerLeanProver/MerLean/tree/master/.claude/skills/plan-graph

## Install

```sh
agentstack add skill-merleanprover-merlean-plan-graph
```

Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent.

## About

# plan-graph — drive the Mem0-g statement plan

The plan (every statement + its dependencies + status) lives in a Mem0 2.x graph, not in
`statements.json`. Each statement is one node; the `dependencies` adjacency IS the graph and
is kept equal to the real Lean dependency graph by `sync-lean`. You drive it through one CLI.
The graph also holds **informal notes** (`type: "Note"` — research conclusions with
provenance, see below): searchable next to the formal statements but excluded from the
dependency graph, topo/levels, dashboard, export, and Lean sync.

## Invocation
Always use the shared `.venv` python, from the repo root (Windows/Git Bash:
`.venv/Scripts/python.exe`):
```
.venv/bin/python src/cli.py --data   [...]
```
(Set up the venv once with the `init_merlean` skill; deps are pinned in `src/requirements.txt`.)

All commands — read-only queries and mutations alike — go through the CLI below. The store
lock is held only per call, so reads are safe from subagents.
`` is the **data folder next to the target file** (`_data/`, or `/datas/`
for a whole library). It holds the graph (`qdrant/` + `history.db`) plus the auto-written
`statements.json`, `progress.json`, and `analytics.json`. (`seed-sorries` derives ``
from the file and prints it.) Output is JSON on stdout; the OpenAI key is read from `.env`
(or the `OPENAI_API_KEY` env var).
The data folder is git-ignored — nothing is stored inside the package.

## Commands
| Command | Use |
|---|---|
| `import-json PATH` | seed the graph from an existing `statements.json` (+ sibling progress/corrections) |
| `export-json [--out P]` | materialize `statements.json` + `progress.json` (debug / interop) |
| `list [--status S] [--kind K]` | all nodes (id/type/name/status/deps) — your overview. `--kind formal\|informal\|all` (default `all`); `--kind informal` reviews the banked notes |
| `get SID` | one node, full metadata (content, proof, anchor, deps, mathlib_types, status, …) |
| `topo` | statement ids in dependency order (deterministic) — the formalization order |
| `cone SID [SID...]` | forward (downstream) dependency cone — what to invalidate when SID changes |
| `cycles` | dependency cycles (must be `[]`) |
| `levels` | statements grouped by dependency layer (level 0 = no deps; same-level = independent) — the **parallel formalization schedule** (≤ 4 background compile-fix subagents at a time; see formalize/prove) |
| `set-status SID STATUS` | `pending` / `in_progress` / `completed` / `completed_axiom` / `failed` |
| `add --json '{"id":...}'` | add a node — a formal statement, or an informal Note (see "Informal notes") |
| `update SID --json '{...}'` | merge fields into a node (deps, content, anchor, corrections, …) |
| `delete SID` | remove a node |
| `sync-lean LIB_DIR` | **rewrite edges from the real `.lean` files** — run after every Lean change |
| `reconcile LIB_DIR [--build]` | **re-derive each node's `status` from its `.lean` file** (no `sorry` ⇒ `completed`, `axiom` ⇒ `completed_axiom`); self-heals the Mem0-g store's status drift. Prefer over trusting stored status; `--build` also requires `lake build` to pass |
| `lint` | **flag top-level decl names defined by >1 node** — a latent clash (ambiguous in any file importing both; a proof can bind the wrong one). Run after `sync-lean`; output `"n": 0` is clean |
| `seed-sorries FILE --lib-dir D` | prove mode: seed a file's `sorry`s (derives `--data` from FILE, prints it) |
| `record SID --role R --json '{}'` | append a subagent metric (tokens/tool_uses/duration_ms) to `analytics.json` |
| `status` | **readable progress dashboard** — counts, % done, per-statement status (the human view) |
| `analytics [--plain]` | `analytics.json` (`--plain` = readable per-statement token/time summary) |
| `summarize` | LLM narrative summary of the plan → `summary.md` + a searchable `Summary` meta-node (excluded from the graph/status) |
| `visualize [--lib-dir D] [--out P] [--format F]` | render the graph as a Graphviz diagram (default into ``) |
| `search "QUERY" [--top-k N] [--retrieve-k K] [--no-rerank] [--kind K]` | semantic search — find nodes by MEANING. See "Semantic search" below. |
| `reset` | wipe the `` folder |

## Node fields
`statement_id, type, name, content, dependencies[], dependents[], proof, anchor,
mathlib_types, lean_path, hierarchy_level, corrections[], status, do_not_import[],
declarations_defined[], imports[], source_start, source_end`.
- `status` replaces progress.json: a statement is "done" when `completed`/`completed_axiom`.
- `dependencies` is the source of truth for ordering and cone invalidation (node/file level).
- `declarations_defined`, `imports`, `source_start/end` are **derived by `sync-lean`** (recomputed
  every run) and kept in Mem0 — they're small and the dashboard/`lint` read them. `dependencies`
  stays the authoritative file-level edge set used for ordering/cones.

## Informal notes (`type: "Note"`)
A note is a **belief with evidence**, not a proven fact: an `explore` subagent's research
answer, a counterexample found, a dead proof approach, a measured threshold. Notes are
embedded for `search` (the `informal` group) but excluded from everything structural
(topo/levels/cone/status/export/sync-lean/lint). Canonical payload:
```
add --json '{"id": "Note_", "type": "Note", "name": "",
  "content": "",
  "confidence": "high|medium|low",
  "source": "explore:  | orchestrator: during  | user",
  "evidence": "", "method": "",
  "caveats": "", "related": ["Thm_Main"]}'
```
Rules:
- **Only the orchestrator (main context) writes notes** — it curates what enters the store
  (subagents read; compile-fix's one mutation stays `sync-lean`).
- **`related`, never `dependencies`**: links to formal nodes are informational only. A formal
  node must NEVER list a Note in its `dependencies`.
- **On conflict, the note yields**: kernel-checked Lean results always beat notes. `update`
  the note (append the old belief + why it fell to `corrections`) or `delete` it. `add`/
  `update` stamp `created`/`updated` automatically.
- Notes get `status: "n/a"` and never appear in the dashboard or `statements.json`.

## Semantic search (`search`) — find nodes by MEANING, not exact name
Retrieval follows LeanSearch-v2's shape: an **embedding stage** (OpenAI) recalls candidates
over each node's informal+formal text, then an **LLM reranker** reorders them per group.
Rerank is on by default and matters — embedding order alone is often imperfect on short,
jargon-dense statements.
```
.venv/bin/python src/cli.py --data  \
    search "" [--top-k N] [--retrieve-k K] [--no-rerank] [--kind K]
```
- `--top-k` (default 5) — results returned **per group**.
- `--retrieve-k` — embedding candidates to rerank (default `max(top_k*6, 30)`).
- `--no-rerank` — pure embedding similarity (faster, lower precision).
- `--kind formal|informal|all` (default `all`) — restrict to one group (skips the other
  group's rerank call).

Output is JSON with **two separately-ranked groups**:
```
{"formal":   [ {statement_id, name, type, status, embed_score, rerank_score, content}, ... ],
 "informal": [ { ...same fields..., confidence, source, updated}, ... ]}
```
`formal` = statement nodes (importable, citable as dependencies). `informal` = notes and the
plan summary — **beliefs with evidence, not proven facts**: use them as leads, never as
dependencies (see "Informal notes" above).

**When to search:**
- **Before adding any statement**: `search ""` — reuse an
  existing node instead of duplicating.
- **Before re-researching anything**: the `informal` group is the project's banked knowledge
  (prior explore answers, dead approaches, counterexamples) — check it before dispatching an
  `explore` subagent or re-deriving a conclusion.
- **Find the right lemma** to apply or depend on; **surface related statements** when
  decomposing or rephrasing.

Search notes: each store is small (one library/proof), so search is scoped to its
``. Embedding model `text-embedding-3-large` (3072 dims); reranker `gpt-4o-mini` (override
`PLAN_RERANK_MODEL`); key from `.env` / `OPENAI_API_KEY`. For exact-structure navigation
(order, status, cones) use `topo`/`list`/`get`/`cone` — search is for meaning, not structure.

## Common recipes
- **Next statement to formalize:** `topo`, then pick the first id whose `status` is `pending`
  and whose `dependencies` are all `completed`/`completed_axiom` (`get` each to check).
- **Mark done:** after a file builds clean AND passes its faithfulness check →
  `sync-lean LIB_DIR` (edges), then `reconcile LIB_DIR` (re-derive status from the files —
  self-healing). **Prefer `reconcile` over a bare `set-status SID completed`:** the Mem0-g store can
  silently revert a written status, and any later full-node write (even `sync-lean`) can lock the
  stale value in; deriving status from the `.lean` files is drift-proof. (`set-status SID in_progress`
  is still used to mark a node as being worked — `reconcile` leaves `sorry`-bearing files untouched.)
- **A statement changed (correction/rephrase):** `cone SID` → for each id in the cone,
  `set-status  pending` and delete its `.lean` file, so the loop re-formalizes the
  downstream cone. Then re-`sync-lean`.
- **After ANY plan edit:** run `cycles` (must be `[]`) and `sync-lean` so the stored graph
  never drifts from the Lean files, **then `visualize`** to regenerate `graph.png`/`graph.dot` so
  the picture always matches the just-updated `statements.json`. Run `lint` (after `sync-lean`)
  whenever you add helper nodes — it flags a top-level name accidentally owned by two nodes (a
  latent ambiguous-import clash) before it propagates.

## Source & license

This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code.

- **Author:** [MerLeanProver](https://github.com/MerLeanProver)
- **Source:** [MerLeanProver/MerLean](https://github.com/MerLeanProver/MerLean)
- **License:** Apache-2.0

Install and usage instructions live in the source repository linked above.

## Pricing

- **Free** — Free

## Security capabilities

Automated source analysis of v0.1.0 — what this tool can access:

- **Network access:** no
- **Filesystem access:** no
- **Shell / process execution:** no
- **Environment & secrets:** yes
- **Dynamic code execution:** no

*"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.*


## Versions

- **0.1.0** — security scan: passed — Imported from the upstream source.

## Links

- Listing page: https://agentstack.voostack.com/l/skill-merleanprover-merlean-plan-graph
- Seller: https://agentstack.voostack.com/s/merleanprover
- Browse the marketplace: https://agentstack.voostack.com/browse

---
Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.