Lean Proof DAG Extractor — Reference

Instructions for LLMs

This section is written for Claude or another LLM working in this codebase. Read it first before touching any file.

What this system is

A tool that extracts the elaborated kernel-level proof term of a Lean 4 theorem as a shared DAG and renders it as a PDF. The DAG is not the source AST or tactic trace — it is the actual Expr value the kernel type-checks.

File map

File	What it does	When to edit
ProofDagExtract.lean	Lean script: loads env, traverses Expr, emits JSON	Change DAG structure, node fields, server protocol
lean_expr_dag.rb	Ruby: spawns Lean, parses JSON, auto-detects modules	Change Ruby API, add auto-detection logic
make_dag_pdf.rb	Ruby: Graphviz DOT + Prawn PDF	Change visual rendering, colours, labels
test_repo/Analysis/SucEven.lean	Example proofs (inductive N/IsEven, no Mathlib)	Add new example theorems
test_repo/Analysis/FourIsEven.lean	Earlier example with numeric literals	Reference only

Critical design decisions — do not break these

1. bvar nodes are never memoised. Expr.bvar 0 is structurally identical everywhere, so the ExprMap memo would merge variables from different enclosing binders. Each bvar occurrence emits a fresh node via emitNodeNoMemo. Do not revert this.

2. N-ary app collapse. Expr.getAppFn/getAppArgs collapse left-nested app(app(f,a),b) chains into one node with flat children. children[0] is always the function; children[1..] are arguments.

3. N-ary lam collapse. peelLams collapses consecutive lam binders. Stops early if an inner lam is already in the memo (shared elsewhere).

4. forall / impl split. forallE is split into forall (body uses the variable: body.hasLooseBVar 0 = true) and impl (body does not). Only consecutive binders of the same kind are collapsed by peelForalls.

5. buildDag, peelLams, peelForalls are in a mutual block because they call each other.

6. Server protocol is line-oriented. All JSON uses Json.compress (compact single line). Never use toString on Json — it produces multi-line output that breaks gets on the Ruby side.

7. ctx : Array Expr is the binder-type stack threaded through all recursive calls (innermost first). arity : Nat is the count of outermost lam binders — used to determine is_arg on bvar nodes.

Common mistakes to avoid

• Don't add bvar back to the memo.
• Don't change children[0] = function convention in app without updating Ruby's edge_style logic in dag_to_dot.
• Don't use multi-line JSON anywhere in the Lean server loop.
• forallE in Lean source no longer appears as a kind in the JSON output — it becomes either "forall" or "impl". Don't look for "forallE" in emitted nodes.
• When adding a new node kind in Lean, also handle it in node_dot_label and node_dot_attrs in make_dag_pdf.rb.
• resolve_import_mods now returns a pair [mods, resolved_name], not just mods. Any caller must unpack both values.

How to test changes

cd test_repo
lake build Analysis.SucEven

# Quick sanity check — should print node count
lake env lean --run ../ProofDagExtract.lean \
  --import Analysis.SucEven --theorem SucEven.eight_is_even_v3

# Full PDF generation
cd .. && ruby make_dag_pdf.rb

---

Quick start — any Lean 4 repo

Pass any declaration name — short, partially qualified, or fully qualified. Everything else is automatic.

require_relative '/Users/simon/Desktop/ZEPHYR/PROOF_DAG/lean_expr_dag.rb'
require_relative '/Users/simon/Desktop/ZEPHYR/PROOF_DAG/make_dag_pdf.rb'

repo = '/path/to/your/lean/repo'
name = 'lim_of_power_decay'   # short, dotted suffix, or fully qualified all work

# Extract JSON DAG
data = extract_dag(repo, name)
puts data['theorem']      # => "Chapter6.Sequence.lim_of_power_decay"  (resolved)
puts data['node_count']   # => 2117

# Render PDF
full_name, mod = resolve_declaration_name(repo, name)
make_single_dag_pdf(repo, '/tmp/out.pdf',
  import:  [mod],
  theorem: full_name,
  heading: full_name)

What happens automatically

1. Name resolution — resolve_declaration_name searches all .lean files (excluding .lake/), finds the declaration, walks the namespace stack (namespace X / end X / end), and returns the fully-qualified name and module. So lim_of_power_decay, Sequence.lim_of_power_decay, and Chapter6.Sequence.lim_of_power_decay all work.

2. Module detection — the file path is converted to a dotted module name (Analysis/Section_6_5.lean → Analysis.Section_6_5).

3. Mathlib cache — if lakefile.lean contains require mathlib and fewer than 100 Mathlib oleans are present, lake exe cache get runs first.

4. Build — if the module's .olean is missing, lake build <module> runs.

If auto-detection fails (macro-generated names, generated files), pass :import => ['Module.Name'] explicitly.

---

Ruby API

extract_dag(repo_path, theorem_name, opts = {})

Spawns one Lean process. For many theorems from the same repo use server mode.

data = extract_dag(repo, 'MyTheorem',
  import:    ['Analysis'],      # auto-detected if omitted
  unfold:    ['SomeConstant'],  # expand these constants inline (optional)
  skeleton:  true,              # suppress Eq.subst/cast/id noise (optional)
  json_file: '/tmp/out.json')   # also write pretty JSON here (optional)

Server mode

Lean env load takes 6–30s depending on imports. Pay it once:

srv = start_dag_server(repo, ['Analysis.SucEven'])
# blocks until Lean prints {"status":"ready"}

d1 = extract_dag_from_server(srv, 'SucEven.eight_is_even_v3')
d2 = extract_dag_from_server(srv, 'SucEven.even_sum',
       unfold: ['SucEven.even_sum'])

stop_dag_server(srv)

Each query after the first takes ~1ms.

resolve_declaration_name(repo_path, name)

Returns [full_qualified_name, module_name]. Used internally by extract_dag but also callable directly when you need both pieces.

dag_stats(data)

dag_stats(data)
# => {
#   theorem:     "SucEven.eight_is_even_v3",
#   root_id:     13,
#   node_count:  14,
#   edge_count:  18,      # total child references
#   shared_refs: 4,       # child ids referenced more than once
#   const_deps:  6,       # distinct const nodes
#   by_kind:     {"const"=>6, "app"=>8},
#   options:     {"skeleton"=>false, "unfold"=>[]}
# }

compare_dags / compare_dags_from_server

cmp = compare_dags(repo, 'Thm.v1', 'Thm.v2', import: ['Analysis'])

cmp[:jaccard]        # 0.0–1.0 similarity of const-name sets
cmp[:shared_consts]  # const names in both
cmp[:only_in_a]      # consts unique to v1
cmp[:only_in_b]      # consts unique to v2
cmp[:stats_a]        # dag_stats for v1
cmp[:stats_b]        # dag_stats for v2

ensure_built(repo_path, import_mods)

Called automatically. Checks for .olean files, runs Mathlib cache fetch if needed, then lake build for any missing module.

---

JSON output format

{
  "theorem":    "SucEven.eight_is_even_v3",
  "root_id":    13,
  "node_count": 14,
  "const_deps": ["SucEven.N.S", "SucEven.IsEven.step", ...],
  "nodes":      [ ... ],
  "options":    { "skeleton": false, "unfold": [] }
}

Nodes are in post-order: children always have lower IDs than parents. children holds integer IDs, not nested objects — shared sub-terms get one node with multiple parents.

Node kinds

kind	extra fields	children
const	name, levels	—
app	arity	[fn, arg0, arg1, ...] — children[0] is function
lam	binders: [{name,bi},...]	[ty0,...,tyN, body]
forall	binders: [{name,bi},...]	[ty0,...,tyN, body]
impl	binders: [{name,bi},...]	[ty0,...,tyN, body]
letE	binder	[type, val, body]
bvar	bvar_idx, type_label, is_arg	—
fvar	name	—
mvar	name	—
sort	level	—
lit	lit_kind (nat/str), value	—
mdata	—	[inner] (absent in skeleton mode)
proj	proj_type, proj_idx	[inner]

bvar fields in detail:

• bvar_idx — De Bruijn index: 0 = innermost enclosing binder, 1 = next out
• type_label — short head name of the binder's type ("N", "IsEven", "_->_")
• is_arg — true if this variable is one of the theorem's own arguments

forall vs impl: both come from Lean's forallE constructor. forall means the body uses the bound variable (body.hasLooseBVar 0 = true). impl means it doesn't — it's a plain implication T → U.

binder_info values: default (explicit), implicit, strict, inst (typeclass).

---

Extraction options

:unfold / --unfold Name1,Name2

Replaces named constants with their definitions before building the DAG. The unfolded names disappear from const_deps; their expanded sub-DAGs appear inline. One level of expansion only — not transitive.

# See the internals of even_sum within eight_is_even_v3
data = extract_dag(repo, 'SucEven.eight_is_even_v3',
         unfold: ['SucEven.even_sum'])
# node_count grows from 14 to 109

:skeleton / --skeleton

Suppresses rewrite/transport boilerplate by replacing these head constants with their last argument:

Eq.subst, Eq.mp, Eq.mpr, cast, id, Eq.symm, Eq.trans, congrArg, congrFun, Eq.refl, rfl, of_eq_true, trivial, propext

Also strips mdata nodes. Useful when you care about logical structure, not the equality proofs used to move types around.

---

Worked example: "Four is even"

Two proofs of the same theorem to illustrate how the DAG differs.

-- test_repo/Analysis/FourIsEven.lean
namespace FourIsEven
def isEven (n : Nat) : Prop := ∃ k, n = 2 * k
theorem two_is_even : isEven 2 := ⟨1, rfl⟩

-- Proof 1: even + 2 is even
theorem even_add_two (n : Nat) (h : isEven n) : isEven (n + 2) :=
  let ⟨k, hk⟩ := h; ⟨k + 1, by omega⟩
theorem four_is_even_v1 : isEven 4 :=
  even_add_two 2 two_is_even

-- Proof 2: sum of two evens
theorem even_sum (m n : Nat) (hm : isEven m) (hn : isEven n) : isEven (m + n) :=
  let ⟨j, hj⟩ := hm; let ⟨k, hk⟩ := hn; ⟨j + k, by omega⟩
theorem four_is_even_v2 : isEven 4 :=
  even_sum 2 2 two_is_even two_is_even
end FourIsEven

srv = start_dag_server(repo, ['Analysis.FourIsEven'])
v1 = extract_dag_from_server(srv, 'FourIsEven.four_is_even_v1')
v2 = extract_dag_from_server(srv, 'FourIsEven.four_is_even_v2')
dag_stats(v1)  # {node_count: 12, shared_refs: 1, ...}
dag_stats(v2)  # {node_count: 14, shared_refs: 3, ...}

The source code of v2 writes two_is_even twice, but in the elaborated proof term it is a single node referenced twice — DAG sharing. shared_refs: 3 reflects: the literal 2 (used twice in typeclass resolution), the elaborated 2 (first and second numeric argument are the same expression), and two_is_even itself.

cmp = compare_dags_from_server(srv,
        'FourIsEven.four_is_even_v1',
        'FourIsEven.four_is_even_v2')
cmp[:jaccard]        # => 0.67
cmp[:shared_consts]  # => ["FourIsEven.two_is_even", "Nat", "OfNat.ofNat", "instOfNatNat"]
cmp[:only_in_a]      # => ["FourIsEven.even_add_two"]
cmp[:only_in_b]      # => ["FourIsEven.even_sum"]

After unfolding two_is_even, similarity rises to 0.82 — the two proofs share all of the two_is_even internals and differ only in their top-level lemma:

cmpu = compare_dags_from_server(srv,
         'FourIsEven.four_is_even_v1', 'FourIsEven.four_is_even_v2',
         unfold: ['FourIsEven.two_is_even'])
cmpu[:jaccard]  # => 0.82

---

Understanding the expression language

Lean's kernel uses the Calculus of Inductive Constructions. Every proof is an Expr value in this language.

Key concepts

De Bruijn indices: Lean doesn't store variable names in the kernel — it uses indices. bvar 0 means "the variable bound by the innermost enclosing binder". bvar 1 means the next one out. Binder name fields (binder, binders[i].name) are display hints only; two expressions that differ only in binder names are structurally identical and share a DAG node.

Lean's kernel is unary: f a b c is stored as app(app(app(f,a),b),c). The DAG collapses these chains using Expr.getAppFn/getAppArgs. Similarly fun x y => body is three nested lam nodes collapsed to one.

forallE is dual-purpose: it is both the universal quantifier and the function arrow. The split into forall/impl kinds makes this distinction visible. In proofs, impl nodes typically carry hypotheses (P → Q) while forall nodes bind variables actually used in the body (∀ n : N, ...).

Propositions are types, proofs are values: IsEven.zero : IsEven Z is both a constructor and a proof. const nodes with proof-constructor names are the axioms of the argument.

brecOn / course-of-values recursion: recursive theorems are compiled by Lean into calls to TypeName.brecOn. This brings in below binders and induction-hypothesis bundles. These appear in unfolded DAGs as lam/forall nodes with high-index bvars and _->_ type labels.

Why N.add appears as a leaf: even_sum has result type IsEven (m.add n). The term N.add appears in that type expression even though addition is not a proof step — it is part of the thing being proved.

Binder info

Value	Lean syntax	Meaning
default	(x : T)	Explicit — caller provides
implicit	{x : T}	Inferred by unification
strict	⦃x : T⦄	Inferred, delayed until next explicit arg
inst	[inst : C]	Filled by typeclass search

---

PDF rendering

make_dag_pdf — side-by-side comparison

make_dag_pdf(repo, 'out.pdf',
  import:    ['Analysis.SucEven'],
  theorem_a: 'SucEven.eight_is_even_v1',
  theorem_b: 'SucEven.eight_is_even_v3',
  title_a:   'Proof 1: chain',
  title_b:   'Proof 3: sum-of-sums',
  heading:   'IsEven 8 — two strategies',
  name_map:  { 'SucEven.IsEven.step' => 'Step Axiom',
               'SucEven.even_sum'    => 'Sum Theorem' },
  unfold_a:  [],
  unfold_b:  [])

make_single_dag_pdf — full-page single theorem

make_single_dag_pdf(repo, 'out.pdf',
  import:   ['Analysis.SucEven'],
  theorem:  'SucEven.eight_is_even_v3',
  title:    'Proof 3 with Sum Theorem expanded',
  heading:  'IsEven 8',
  name_map: { 'SucEven.even_sum' => 'Sum Theorem' },
  unfold:   ['SucEven.even_sum'])

name_map

Maps full Lean names to display labels. Any const whose name is a key gets a blue "proof component" box and the display label. Everything else is grey "machinery".

Colour scheme

Colour	Meaning
Blue rounded box	Named proof component (in name_map)
Grey box	Internal machinery const
Green ellipse	Binder: F = fun, forAll = universal, let
Purple ellipse	Implication (->)
Red ellipse	Theorem argument variable (is_arg = true)
Orange ellipse	Internal bound variable
Yellow box	Literal
Orange border	Node referenced >1 time (DAG sharing)
Thick black border	Root node
Solid edge	Function position in app
Dashed edge	Argument, binder type, or body

node_dot_label label conventions

kind	label
const	name_map value, or last dotted component
app	@ (arity 1) or @N (arity N)
lam	F x y z (binder names, _ for hygienic names)
forall	forAll x y
impl	-> or -> (xN) for N-ary
bvar	type_label (e.g. N, IsEven, _->_)
sort	Sort 0 / Sort 1 etc.

Hygienic binder names (matching /_@_|_hyg_|_hygCtx_/) are replaced with _.

---

Architecture notes

• ProofDagExtract.lean only needs import Lean. It loads user modules at runtime via Lean.importModules — no changes to user lakefile.lean needed.
• Run under lake env so LEAN_PATH is set and .olean files are found.
• ExprMap (structural Expr equality) drives DAG sharing — identical sub-expressions get one node id. Exception: bvar nodes, which are never memoised (see LLM instructions above).
• const_deps is extracted from the emitted node array, not the original Expr. After unfolding, the original constant is absent and its expanded dependencies appear instead.
• countOuterLams counts leading lam binders on the proof value to determine theorem arity before traversal begins.