Skip to content

Lean 4 export: GDS architecture is naturally suited for theorem prover formalization #76

@rororowyourboat

Description

@rororowyourboat

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions