Skip to article frontmatterSkip to article content
Site not loading correctly?

This may be due to an incorrect BASE_URL configuration. See the MyST Documentation for reference.

WG1 — SCE Working Group on Language, Calculus & Formal Semantics

Part of the Research Program for AI as Babel Fish for Structural Economics.

Chair: Akshay Shanker (designated June 2026).

Scope

This working group addresses the semantic specification of dynamic structural models: the economist-facing declarative language; the typed Bellman-core and its denotational semantics; and, where feasible, a formal encoding of that semantics in Lean. The three layers are mutually dependent — a usable language requires an explicit semantics; an explicit semantics is scientifically meaningful only if it can be stated in a shareable language; and a formal encoding makes model meaning machine-readable and checkable against a shared knowledge base.

Aims

Develop a software-independent declarative language in which a discrete-time Bellman model is written once — mathematically explicit, modular, and free of numerical content — and elaborate it to a single typed core object (a “Bellman-core” / term-graph) with denotational semantics. Encode that semantics, in parallel, in a machine-readable form (Lean), as part of a formal knowledge base of standard dynamic-programming theory, so that specifications can be type-checked against encoded background results rather than judged by informal argument alone.

Scientific rationale

Structural papers typically ship bespoke codebases in which the model on paper is not formally bound to the implementation. A shared declarative language is a prerequisite for reproducibility, interoperability, AI-assisted authoring, and systematic robustness analysis: each requires a portable representation of the model itself, independent of any particular solver or codebase. A formal semantic core makes statements such as “this method preserves the solution” or “these two formulations are equivalent” mathematically precise; a formal knowledge base connects the program to the broader AI-for-Science / formalization literature (the economics analogue of formalizing physics in Lean; see prior art §5).

Current state

Surface language (from bellman-ddsl)

Formal core

Machine formalization

Registries: stage, period, and trellis libraries

Because models are assembled from reusable, composable components, the language should support three curated, versioned catalogs: a stage registry (single arrival→decision→continuation problems), a period registry (named compositions of stages), and a trellis registry (multi-period composites). Components should be discoverable, versioned, citable, and safely recombinable. At present these exist per application; the research agenda calls for program-wide shared registries.

Cross-subfield integration (representation)

Letting models and components from different economics traditions — heterogeneous-agent macro, structural microeconometrics, computable general equilibrium (CGE), agent-based modeling (ABM), and applied IO — be expressed, shared, and coupled in one representation is a cross-cutting aim of the program. WG1 owns its representational half:

The numerical side of this agenda (Rosetta Stones to CGE/ABM/IO toolkits, verification of coupled models) sits in WG2; AI-assisted translation of subfield papers and cross-subfield reproducibility sit in WG3. See prior art §6 for cross-field precedents (OpenKIM, ESMF, OPTIMADE, …).

Precedent: PhysLean / mathlib

Physics and mathematics provide the closest precedent for the formal encoding layer. mathlib is the community formal-mathematics library in Lean; PhysLean/Physlib formalizes physics in Lean 4; Lean4PHYS / LeanPhysBench add a foundation library and a benchmark for formal physics reasoning by language models. Two findings are directly relevant: (i) a field requires its own formal corpus and notation (math-specialized formal libraries did not transfer to physics); and (ii) providing the formal library as context measurably improves model accuracy — an empirical argument for grounding the AI work in WG3 in this formal layer.

Five-year milestones

Open research questions

Illustrative project proposals

Extend the language to discrete-continuous (branching) choice: specify the surface syntax and elaboration for discrete regime choice (participation, default, retirement timing), validate against three published life-cycle models, and contribute the grammar extension and test suite.

Build a Lean foundation library for modular dynamic programming: define the core types, encode standard existence and convergence results from the DP literature, and release an open EconDP benchmark for evaluating AI-assisted formalization.

Indicators of progress

Specification version cadence; adoption of the Bellman-core IR as the input to downstream tooling; breadth of models expressible in the language; registry size and reuse; coverage of the formal knowledge base (encoded standard results and model encodings); adoption of the EconDP benchmark; models authored by researchers outside the core team; consumption of the spec by backends (joint with WG2).

Potential funding sources

NSF (cyberinfrastructure / economics; CISE / Foundations of computing; AI for science), JHU DS/AI Institute, FRO/Convergent, philanthropy (cf. the Lean/mathlib gifts).

Foundations

Bellman (DP origins); Sargent–Stachurski (recursive methods, contraction/monotone theory); Backus FFP (composition, meaning vs. representation); category-theoretic semantics; dolo lineage (Winant); Lean 4 + mathlib and the PhysLean/Lean4PHYS precedent.

Research Program for AI as Babel Fish for Structural Economics
Prior Art: Interoperable-Tooling Research Programs in Other Disciplines
Research Program for AI as Babel Fish for Structural Economics
WG2 — SCE Working Group on Methods, Backends & Verification