Econlib
A Lean 4 library for economic and political theory.
Econlib formalizes economic and political theory in Lean 4 — preferences, probability, optimization, game theory, mechanism design, social choice, general equilibrium, and the supporting mathematics — with an API designed to help you formalize your research.
About Econlib
An introduction to Econlib's design principles, scope, key results, and future plans.
The full library source and issue tracker.
Using Econlib
To install Lean, see the
Lean website. Once you have set up
a project, add Econlib as a dependency in your lakefile.toml:
[[require]]
name = "econlib"
git = "https://github.com/danlyng/Econlib"
rev = "main"The additional resources below may also be useful.
Hybrid lexical + dense retrieval over Econlib and its Mathlib dependency.
Type- and pattern-based search over Econlib, Mathlib, and Lean by shape, constant, or subexpression.
Guidance for using Econlib with coding agents.