Context
GDS's architecture maps remarkably well to Lean 4's dependent type system. The structural invariants enforced at runtime by Pydantic validators are exactly what Lean encodes at the type level — making the lift from Python to Lean largely mechanical rather than conceptual.
Why GDS is a natural fit for Lean
| GDS Python |
Lean 4 Equivalent |
| Sealed Block hierarchy (5 types) |
inductive Block with 5 constructors |
@model_validator invariants |
Dependent types / proof fields in structure |
| Token overlap auto-wiring |
(out.tokens ∩ inp.tokens).Nonempty as decidable Prop |
BoundaryAction (no inputs) |
h_role : inputs = ∅ proof field |
TemporalLoop covariant-only |
h_dir : ∀ w ∈ ws, w.direction = COVARIANT proof field |
| G-001..G-006 verification checks |
Decidable propositions discharged by by decide |
Canonical h = f ∘ g |
Function + theorem proving decomposition holds |
What Mathlib already provides
- Symmetric monoidal categories —
>> maps to categorical composition, | maps to tensor product ⊗. Coherence laws (associativity, braiding) are already proven.
Finset String — token sets with decidable equality, intersection, subset.
Function.comp — direct support for the canonical form.
- Graph theory basics — for G-006 DAG acyclicity.
What's missing (and how close it is)
- No strategic game theory in Mathlib — Mathlib's
SetTheory.Game is Conway combinatorial games, not normal-form/strategic games. A community project (formalizing-game-theory) has Lean 4 definitions for PureStrategy, MixedStrategy, StrategyProfile, and IsNashEquilibrium.
- No open games formalization exists in any proof assistant (Lean, Coq, Agda). Formalizing Hedges' compositional game theory as an SMC in Lean would be a novel research contribution.
Incremental path forward
Tier 1 — Structural export (weeks)
- ~200-line
GDSLean Lean 4 library defining Block, SystemIR, WiringIR with proof fields
- Python
lean_export() on SystemIR emitting syntactically correct Lean
- All 6 generic checks become compile-time proof obligations that
decide auto-discharges
- Prisoner's Dilemma as first test case
Tier 2 — Categorical proofs (months)
- Prove GDS composition forms a symmetric monoidal category
- Canonical
h = f ∘ g as a formal decomposition theorem
- OGS bridge as a functor from
OpenGame SMC → GDSSpec SMC
Tier 3 — Open games formalization (research frontier)
OpenGame (X R S Σ) with play, coplay, bestresponse
- Nash equilibrium preservation under composition
- Nash existence via Brouwer fixed-point (requires heavy real analysis from Mathlib)
Key references
Context
GDS's architecture maps remarkably well to Lean 4's dependent type system. The structural invariants enforced at runtime by Pydantic validators are exactly what Lean encodes at the type level — making the lift from Python to Lean largely mechanical rather than conceptual.
Why GDS is a natural fit for Lean
inductive Blockwith 5 constructors@model_validatorinvariantsstructure(out.tokens ∩ inp.tokens).Nonemptyas decidablePropBoundaryAction(no inputs)h_role : inputs = ∅proof fieldTemporalLoopcovariant-onlyh_dir : ∀ w ∈ ws, w.direction = COVARIANTproof fieldby decideh = f ∘ gWhat Mathlib already provides
>>maps to categorical composition,|maps to tensor product⊗. Coherence laws (associativity, braiding) are already proven.Finset String— token sets with decidable equality, intersection, subset.Function.comp— direct support for the canonical form.What's missing (and how close it is)
SetTheory.Gameis Conway combinatorial games, not normal-form/strategic games. A community project (formalizing-game-theory) has Lean 4 definitions forPureStrategy,MixedStrategy,StrategyProfile, andIsNashEquilibrium.Incremental path forward
Tier 1 — Structural export (weeks)
GDSLeanLean 4 library definingBlock,SystemIR,WiringIRwith proof fieldslean_export()onSystemIRemitting syntactically correct Leandecideauto-dischargesTier 2 — Categorical proofs (months)
h = f ∘ gas a formal decomposition theoremOpenGameSMC →GDSSpecSMCTier 3 — Open games formalization (research frontier)
OpenGame (X R S Σ)withplay,coplay,bestresponseKey references