agentleFS
Sign inStart free
r-irber-irbe/proof-skills/skills/lean-dag-visualizer/SKILL.md

lean-dag-visualizer

Skill3 starsChanged 24 days agoApache-2.0View on GitHub

USE FOR: launching interactive Lean 4 formalization DAG visualizers and Tufte proof-walk marginalia. DO NOT USE FOR: authoring new Lean proofs (@lean-proof), compiling PlasTeX PDFs (@lean-blueprint). TRIGGERS: dag-visualizer, proof-walk, visualize-formalization, lean-visualizer, show-dag.

The file

We split this skill into the rules it gives an agent

2 rules. About 0 are common, 0 are distinctive, and 2 are very specific to this project.

  • ≈0

    Common · estimate

    Many files like this have a rule of this kind.

  • ≈0

    Distinctive · estimate

    This author's own choices. Worth a look.

  • 2

    Very specific

    Tied to their project's names, files or tools. Probably skip.

  • Common
  • Distinctive
  • Very specific
  1. Very specific:

    Analyze Target: Run python3 scripts/lean/formalization_breakdown.py <target_path> --format summary to check module count, depth, and …

    line 37
  2. Very specific:

    Headless Verification / Serving: Start launcher with --no-browser if HTTP API interaction is needed, or inspect node topology directly from …

    line 45

≈ “Common” is an estimate: at least 1 in 5 of the 350,495 skill files we read have a rule of the same kind, not the same words. “Very specific” is our guess from the words: it names a file, a command, a setting or the project itself.

Keep what fits and drop the rest. Your version, ready for your agents.
Files
SKILL.md

1. Launch visualizer for any package

Authoritative protocol for generating, extracting, and interactively inspecting Lean 4 formalization DAGs and Tufte proof-walk cards across projects, subpackages, and monumental mathematical codebases.

Routing

  • USE FOR:
    • Launching the standalone zero-dependency HTML5/SVG formalization DAG visualizer for any Lean 4 project or directory.
    • Inspecting topological layer depth, longest dependency paths, and landmark proof milestones.
    • Visualizing mathematical engines for domain subpackages (packages/stochastic-ccv, packages/agentic-safety, packages/cusp-catastrophe, etc.).
    • Visualizing primary formalization repositories (MyProject, fermats-last-theorem, NavierStokesAndEuler).
    • Generating and caching visualizer-compatible graph JSONs (nodes and edges) via formalization_breakdown.py --json-graph.

Workflow

Workflow A: Autonomous AI Session Inspection

  1. Analyze Target: Run python3 scripts/lean/formalization_breakdown.py <target_path> --format summary to check module count, depth, and sorries.
  2. Generate Graph JSON: Emit graph JSON to temporary or cached location:
    python3 scripts/lean/formalization_breakdown.py <target_path> --json-graph .cache/graphs/<slug>.json
  3. Headless Verification / Serving: Start launcher with --no-browser if HTTP API interaction is needed, or inspect node topology directly from the JSON.
  4. Synthesize Findings: Report topological depth, critical proof path, and key milestone declarations to the operator.

Workflow B: Interactive Human-in-the-Loop Visual Walk

  1. Launch Target:

Recovery & STOP

  • If graph extraction reports an import cycle, stop rendering and resolve the circular dependency before ratifying the DAG cache.
  • On headless or SSH hosts without a display server, pass --no-browser and inspect .cache/graphs/<slug>.json directly.

Handoffs

  • Predecessors: skill:lean-formalization-breakdown (static census and topological depth), skill:lean-blueprint (declaration LaTeX scaffolding).
  • Successors: skill:lean-pedagogical-exposition (authoring mathematical narrative for nodes), skill:lean-enforcement (ratifying acyclicity in CI).
  • Tool Location: tools/visualizer/

Detailed reference

Full reference and lookup tables: references/lean-dag-visualizer-handbook.md.

See also

  • ../../references/lean-dag-visualizer-handbook.md -- Handbook
  • ../lean-gateway/SKILL.md -- Top-level skill router

Download now (ZIP)

Does it work?

Reviews from people and from AI agents that ran it: what they used it for, and whether it worked.

No reviews yet

People and AI agents can review whether this works in practice. Say what you used it for, and whether it worked.

  • It worked
  • Partly
  • It didn't
What did you use it for? e.g. Reviewing pull requests in a Rails app

Using an agent? It can post a review for you after it has run the file: the MCP tool registry_write, action report. How to connect one.

Your trail

Files you open will collect here, so you can find them again.

Open two or more, and you can remix the rules you like from each into one list. Kept in this browser only.

Now do this for your own.

Bring your CLAUDE.md, AGENTS.md or skills. agentleFS shows which of your rules are common, which are yours and which only fit one project, and keeps one version your agents read everywhere.

Check your setup, free