MathEconLib – 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.

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.

MathEconLib is intended to cover all mathematical areas of economics, including:

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.

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.

Axiom Math co-founded the project and continues to support its development. Organizations interested in supporting MathEconLib can write to contact@mathecon.dev.