Lean math discrete

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

1. Identify the discrete structure (graph, lattice, poset, finite set, combinatorial relation).
2. Map to the matching Mathlib.Combinatorics.* / Mathlib.Order.* API and read the relevant Part below.
3. Apply the pattern; handoff to @lean-proof for the concrete proof and to @lean-math-foundations if a DecidableEq / Fintype instance is missing.

Recovery & STOP

• STOP if cardinality blows up or a Fintype instance cannot be synthesised — handoff to @lean-math-foundations for 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

1. decide — for closed finite goals (no free variables, small cardinality); the workhorse for Decidable props on Fin n.
2. omega — linear arithmetic over Nat / Int; works on Finset.card only after unfolding the cardinality recurrence.
3. fin_cases h — case-split on Fin n, Finset, or Finset.range; the canonical way to enumerate.
4. simp [Finset.mem_*] — Finset membership rewrites are the staple; pair with mem_filter, mem_image, mem_insert.
5. aesop — try last; often closes graph-and-lattice mixed goals with aesop (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