r-irbe Lean 4 Discrete Mathematics & Graph Theory
Guide to formalizing graphs, lattices, combinatorics, and discrete structures in Lean 4.
Routing
- USE FOR: graph theory, applied lattice theory, combinatorics, DAGs, posets, provenance chains, dependency orders, lattice operations (severity / quality-gate / trust-vector / information-flow lattices), combinatorial bounds, and finite structures in Lean 4. Owns all applied lattice instances.
- DO NOT USE FOR: the abstract algebraic typeclass tower (delegate to
@lean-math-foundations); continuous structures (delegate to@lean-math-analysis); writing one specific proof (delegate to@lean-proof). - TRIGGERS: graph, DAG, lattice, poset, combinatorics, provenance, dependency graph, severity lattice, knowledge graph, finite set bound.
Workflow
- Identify the discrete structure (graph, lattice, poset, finite set, combinatorial relation).
- Map to the matching
Mathlib.Combinatorics.*/Mathlib.Order.*API and read the relevant Part below. - Apply the pattern; handoff to
@lean-prooffor the concrete proof and to@lean-math-foundationsif aDecidableEq/Fintypeinstance is missing.
Recovery & STOP
- STOP if cardinality blows up or a
Fintypeinstance cannot be synthesised — handoff to@lean-math-foundationsfor the instance plumbing. - STOP if the lattice instance you need does not exist at the current Mathlib pin — escalate to
@lean-research, then author the instance under@lean-proof.
Handoffs
- Predecessors:
agent:gateway,skill:lean-proof(mid-proof graph or lattice goal),skill:lean-research(combinatorial result survey). - Successors:
skill:lean-proof(apply the discrete pattern),skill:lean-proof-review(audit the instance),skill:lean-math-foundations(typeclass / decidability plumbing).
Detailed reference
Full encyclopaedia content (Parts 1 through 7) lives in
references/lean4-math-discrete.md. Load that file
when authoring; the SKILL.md only carries the dispatch contract and
the high-frequency pitfalls / recipes (kept inline below).
| Part | Topic | Covers |
|---|---|---|
| Part 1 | Graph Theory in Lean | SimpleGraph, Reachable, Connected, Walk / Path |
| Part 2 | DAG Algorithms | Quiver.Path, topological-sort idioms (no canonical Mathlib tactic) |
| Part 3 | Lattice Theory | Lattice, CompleteLattice, sup_inf distributivity, BoundedOrder |
| Part 4 | Combinatorics | Finset, Multiset, combinatorial identities, choose-sum lemmas |
| Part 5 | Knowledge Graph Formalization | project knowledge-graph + provenance-chain idioms |
| Part 6 | Finite State Machines | Inductive State types, transition relations, reachability |
| Part 7 | Order Theory Extensions | Galois insertions, abstract interpretation patterns |
Part 8 — Research Council Integration
Consolidated into the single canonical routing matrix:
references/research-council-skill-map.md
(see the "Discrete" section). When dispatching a question to a
council member, cite that table rather than restating the rows here.
Part 9 — Common Pitfalls & Quick Tactics
| Pitfall | Symptom | Recovery |
|---|---|---|
Missing DecidableEq on vertex type |
decide / fin_cases fail with failed to synthesize |
derive DecidableEq on the type; or instance : DecidableEq V := …; for adhoc structures use instance : DecidableEq V := by intro a b; cases a <;> cases b <;> simp |
Confusing Finset vs Set |
Finset.mem doesn't fire on a Set goal |
Use Set.toFinset (needs [Fintype]) or rewrite the goal in Finset terms; the two APIs do not mix lemma-by-lemma |
omega fails on a "should be obvious" Finset.card bound |
omega has no card lemmas |
Unfold Finset.card via Finset.card_insert_of_not_mem / Finset.card_image_of_injective first, then omega |
| Lattice instance overlap with foundations | Diamond / "multiple instances" warning | Locally attribute [-instance] foo or move the instance to the right cluster (applied → here, abstract → foundations) |
| Infinite graph snuck in | Decidable synthesis explodes; build hangs |
Add [Fintype V] and re-check the existential / for-all is bounded over a Finset, not a Set |
SimpleGraph vs Graph (multi-edge) confusion |
Theorem statement uses the wrong vertex pair type | SimpleGraph = irreflexive symmetric V → V → Prop; multi-edge graphs need Quiver or hand-rolled types |
Quick reference — top-5 discrete tactics
decide— for closed finite goals (no free variables, small cardinality); the workhorse forDecidableprops onFin n.omega— linear arithmetic overNat/Int; works onFinset.cardonly after unfolding the cardinality recurrence.fin_cases h— case-split onFin n,Finset, orFinset.range; the canonical way to enumerate.simp [Finset.mem_*]— Finset membership rewrites are the staple; pair withmem_filter,mem_image,mem_insert.aesop— try last; often closes graph-and-lattice mixed goals withaesop (add safe simp [Finset.subset_iff]).
Part 10 — Mathlib Cross-Reference Index
Concrete entry-points for the most common discrete-math goals:
| Goal | Mathlib lemma / namespace |
|---|---|
Connectivity in a SimpleGraph |
SimpleGraph.Connected, Reachable |
| DAG / topological sort | Quiver.Path, no canonical topological-sort tactic — author one |
Lattice sup/inf interaction |
Mathlib.Order.Lattice — sup_inf_distrib_left family |
| Galois connection between concrete and abstract | GaloisConnection, GaloisInsertion in Mathlib.Order.GaloisConnection |
| Finset cardinality bound | Finset.card_le_card, Finset.card_image_le, Finset.card_filter_le |
Fintype instance on a structure |
deriving Fintype, DecidableEq (works on most product / sum types) |
| Combinatorial identity | Finset.sum_range_succ, Finset.sum_choose_succ_* (Pascal-rule family) |
See also
../../references/lean4-math-discrete.md— Discrete Mathematics Encyclopaedia (full encyclopaedia, extracted from this skill)../../templates/Template_Arithmetic.md— Template: Nat/Int arithmetic and simplex constraints../../templates/Template_Foundation.md— Template: Decidable predicates and case analysis