MathEconLib – Machine-checked mathematical economics

Academic economists and Axiom Math co-founded MathEconLib in 2026, a shared formal foundation in Lean 4 for machine-checked mathematical economics that builds on Mathlib and aims to cover microeconomic theory, macroeconomic theory and econometrics. The library supplies reusable definitions and theorems for preferences, incentives, equilibrium, dynamics, identification, estimation and inference, with Lean's kernel checking every theorem and human review enforcing design principles; every pull request must build cleanly and contain no `sorry`, `admit` or `native_decide`, and add no axioms beyond the standard three. MathEconLib states it is not an end-to-end autoformalization project, and while researchers may use AI to help with formalization and proof development, economic theorists determine the mathematical architecture.

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 https://axiommath.ai/ 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 https://github.com/leanprover-community/mathlib4 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 https://github.com/matheconlib/matheconlib/blob/main/DESIGN.md . 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 https://github.com/matheconlib/matheconlib/blob/main/docs/BeginnersManual.md - 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 https://github.com/matheconlib/matheconlib/blob/main/docs/PricingArchitecture.md - How the auction layers extend to posted pricing and other single-parameter problems. - MathEconLib README https://github.com/matheconlib/matheconlib/blob/main/README.md - 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 https://github.com/matheconlib/matheconlib/blob/main/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 https://github.com/matheconlib/matheconlib/issues . PRs touching the core layers require a maintainer review before merge. For a first contribution, try documenting the BidderProblem umbrella https://github.com/matheconlib/matheconlib/issues/118 , a small documentation task with a starting file and build instructions. Propose a focused research project Email contact@mathecon.dev mailto: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 https://axiommath.ai co-founded the project and continues to support its development. Organizations interested in supporting MathEconLib can write to contact@mathecon.dev mailto:contact@mathecon.dev .