MathEconLib is an effort to build a shared formal foundation for economics in Lean 4, with the long-term scope of microeconomic theory, macroeconomic theory, and econometrics. Current development focuses on microeconomic theory and its mathematical foundations, building on Mathlib.
Project website · Beginner's manual · Documentation · Contributing
New to Lean or to this library? Lean 4 and MathEconLib — A Beginner's Manual covers installation, reading a real library file, and runnable exercises. It assumes mathematical familiarity but no prior Lean or economics knowledge.
Install Lean and create a Lean project. Match your project's lean-toolchain to the version used by MathEconLib, then add this dependency to your lakefile.toml:
[[require]]
name = "matheconlib"
git = "https://github.com/matheconlib/matheconlib"
rev = "main"From your project directory, fetch the dependency and prebuilt Mathlib files:
lake update
lake exe cache getImport the library in a Lean file:
import MathEconLibFor reproducible projects, replace main with a specific commit and use the toolchain from that revision.
After installing Lean, run:
git clone https://github.com/matheconlib/matheconlib.git
cd matheconlib
lake exe cache get
lake buildThe checkout's lean-toolchain selects the Lean version. The default build checks the library, API stability pins, tests, and worked examples.
The library is organized around shared definitions and results that economic models can reuse. These are broad entry points, rather than an exhaustive module index:
| Area | Selected topics |
|---|---|
| Game theory | Strategic and Bayesian games, pure and mixed Nash equilibria, Nash equilibrium under action translation |
| Mechanism design and auctions | Mechanisms, induced strategic and Bayesian games, incentive compatibility and payment identities, revenue equivalence and auction formats |
| Choice and matching | Choice functions and substitutability, matching with contracts and stable outcomes |
| Pricing | Single-parameter choice, value distributions, posted-price optimality, and comparative statics |
| Mathematical foundations | Probability, order statistics, and supporting analysis, order, and fixed-point results |
Browse the source tree for individual modules and their statements, or see the architecture overview for how the pieces fit together.
- Game theory: matching pennies. A worked example with no pure Nash equilibrium and a unique mixed equilibrium in which both players randomize uniformly.
- Mechanism design: posted-price games. Checked examples derive truthful dominance and Nash equilibrium from DSIC, calculate purchase payoffs, and verify agreement with the induced Bayesian game at fixed true types. A separate interdependent-values example shows that truthful Nash equilibrium at every true type profile need not imply DSIC.
- Pricing: posted prices with uniform buyer values. Optimal pricing within the value-support interval and comparative statics, with concrete checked applications, including the optimal price of
1/2for uniform values on[0, 1]and zero seller continuation value. - Price theory: a Becker-inspired model of crime. A stylized risk-neutral choice model treats the expected sanction as a price, deriving a cutoff rule, individual deterrence results, and aggregate crime under a fixed distribution of net gains.
Worked demonstrations live in MathEconLibExamples/; reusable developments live in the core library, with API and regression checks in MathEconLibTest/.
Contributions of definitions, proofs, worked applications, and documentation are welcome. Start with the design principles and contribution guidelines, which explain where developments belong and when a design discussion is needed.
Browse open issues for ongoing work, or look for a good first issue.
Have you built something using MathEconLib, or would you like to get involved? Reach out at contact@mathecon.dev.
MathEconLib is released under the Apache License 2.0.