EconCSLib is a Lean 4 library and cross-linked knowledge base for computational economics, built on Mathlib.
The initial public release focuses on reusable foundations rather than complete coverage of the field. It includes strategic, extensive, and coalitional games; social choice and fair division; matching; auctions and mechanism design; utility theory; and supporting mathematics such as fixed-point, minimax, and linear-programming results.
| Surface | Link |
|---|---|
| API reference | https://gametheoryinlean.github.io/econcslib_doc/ |
| Knowledge blueprint | https://gametheoryinlean.github.io/blueprint/ |
The blueprint records both formalized material and mathematical targets that still need Lean implementations. The stable Lean import surface contains no deferred proofs.
git clone https://github.com/gametheoryinlean/EconCSLib.git
cd EconCSLib
lake exe cache get
lake build
lake build EconCSLib.ExamplesLean version: leanprover/lean4:v4.30.0
Import the stable library surface with:
import EconCSLibWorked examples live under EconCSLib/Examples/.
Experimental open-problem interfaces under
EconCSLib/OpenProblem/ are opt-in.
docs/design.mddescribes architecture and contribution rules.docs/design/contains focused API notes.docs/research/retains selected mathematical design and proof-strategy notes.docs/maintainers/documents reproducible publishing workflows.docs/knowledge/is the editable source for the generated knowledge blueprint.AGENTS.mdis supplemental guidance for coding agents.
Contributions are welcome. See CONTRIBUTING.md, then browse
the issue tracker or
start a discussion.
AI tools have assisted with routine proof engineering, maintenance, and documentation. Domain contributors remain responsible for reviewing mathematical models, theorem statements, and public API decisions.
EconCSLib grew out of a game-theory formalization project at Xiamen University
Malaysia. See docs/HISTORY.md for a concise project
history.
Coordinators (alphabetical by surname): Bei Xiaohui (NTU), Fu Hongfei, Ma Jiajun (XMUM), Jing Zhan (SJTU).
Contributors: Wang Haocheng, Lü Yuwei (吕宇维), Xing2222, Li Kai, Oh Siew Zher, Ma Yuxuan, Luo Yiding, Timothy Wan (NUS), ARTHURCHOU, abc12321, Hennessy, XGCC666, Zli-Math.
See also nikhgarg/EconCSLib, a separate project with the same name that was developed independently and concurrently. That project focuses on AI-assisted, paper-by-paper formalization of Economics and Computation research, together with workflows for human review of the translation from papers into Lean. This project focuses on the human curation, with AI assistance, of reusable definitions, theorems, and a cross-linked knowledge base for the field. The projects are complementary but are not affiliated.
- Maschler, Solan, Zamir, Game Theory (Cambridge University Press, 2013)
- Nisan, Roughgarden, Tardos, Vazirani, Algorithmic Game Theory (Cambridge University Press, 2007)
- Laraki, Renault, Sorin, Mathematical Foundations of Game Theory (Springer, 2019)
- Krishna, Auction Theory, 2nd ed. (Academic Press, 2009)