Machine-checked mathematical economics.
MathEconLib is an effort to build a shared formal foundation in Lean 4 for research and applications in economics. Co-founded by academic economists and Axiom Math in 2026.
Use existing theorems to prove new ones #
MathEconLib provides shared definitions and reusable results that scholars and practitioners can apply and extend. Researchers can use these building blocks to refine existing economic frameworks, assemble new ones, and prove results about preferences, incentives, equilibrium, dynamics, identification, estimation, and inference.
Library definitions and theorems support many economic models. Lean tracks the assumptions each proof relies on.
MathEconLib builds on Mathlib and encourages upstream contributions of broadly reusable mathematical results.
MathEconLib is not an end-to-end autoformalization project. Its definitions and conventions are developed by economic theorists, with the aim of building a trusted foundation for formal research in economics.
We welcome researchers to use AI to help with formalization and proof development, but researchers determine the mathematical architecture and Lean's kernel checks every theorem. Contributions receive human review for consistency with our design principles.
Long-term scope #
MathEconLib is intended to cover all mathematical areas of economics, including:
- Microeconomic theory
- Preferences and choice, games, information, contracts, market and mechanism design, industrial organization, and general equilibrium.
- Macroeconomic theory
- Dynamic optimization, recursive methods, growth, heterogeneous-agent models, and monetary and fiscal theory.
- Econometrics
- Probability and statistical foundations, identification, estimation, inference, and causal and structural methods.
Documentation #
- Lean 4 and MathEconLib: A Beginner's Manual
- From installing the toolchain to reading the bidder-problem file line by line, with runnable exercises. Assumes no prior knowledge of Lean.
- Pricing Foundations: Mathematical Model and Architecture
- How the auction layers extend to posted pricing and other single-parameter problems.
- MathEconLib README
- Project overview, current coverage, and instructions for using or building the library.
Contributing #
Research questions and new models are welcome in design issues. New theorems in existing chapters, documentation, and applications built on the existing layers can go straight to a pull request. Small, well-scoped additions to the ForMathlib folder can be suitable first contributions.
Changes to the foundational layers start with a design issue: sketch the definitions and main statements and get agreement on the shape before writing proofs. Every pull request must build cleanly, contain no sorry, admit, or native_decide, and add no axioms beyond the standard three.
Lean contributors should read CONTRIBUTING.md for the build, API, and review requirements. New contributors can work through the beginner's manual, improve documentation, or discuss a small task in GitHub Issues. PRs touching the core layers require a maintainer review before merge.
For a first contribution, try documenting the BidderProblem umbrella, a small documentation task with a starting file and build instructions.
Propose a focused research project
Email contact@mathecon.dev or open a design issue. Describe the economic question and relevant literature, the intended definitions and assumptions, the main statement or example to formalize, and the existing library components you expect to reuse. Identify any changes to foundational definitions so the team can agree on the design before proofs are written.
People #
Core contributors
Alphabetical.
- Ruiz ChenAxiom Math[@Ruizsolveall](https://github.com/Ruizsolveall)
- Bo CowgillUniversity of Toronto[@bocowgill](https://github.com/bocowgill)
- Piotr DworczakUniversity of Cologne; Northwestern University; GRAPE[Profile](https://pdworczak.com/)
- Ben EltschigAxiom Math[@peabrainiac](https://github.com/peabrainiac)
- Nikhil GargCornell Tech and Cornell University[Profile](https://gargnikhil.com/)
- Ziv HellmanBar-Ilan University[Profile](https://econ.biu.ac.il/en/hellman)
- Scott Duke KominersHarvard University and a16z crypto[@scduko](https://github.com/scduko)
- Moran KorenBen-Gurion University[@morankor](https://github.com/morankor)
- Daniel LyngPrinceton University[@danlyng](https://github.com/danlyng)
- Ken OnoAxiom Math; University of Virginia (on leave)[Profile](https://uva.theopenscholar.com/ken-ono)
- Jujian Zhang[@jjaassoonn](https://github.com/jjaassoonn)
Supporting organizations
Axiom Math co-founded the project and continues to support its development. Organizations interested in supporting MathEconLib can write to contact@mathecon.dev.