EconCSLib: A Lean Library for Computational Economics and AI-Assisted Research
2026-06-15 • Computer Science and Game Theory
Computer Science and Game Theory
AI summaryⓘ
The authors present EconCSLib, a new Lean 4 library designed to help turn ideas in economics into computer-verified math statements. It focuses on areas like game theory and social choice to build reusable math tools and check proofs carefully. Their work also explores how AI can assist in this process, making it easier to formalize complex economics concepts and open problems. They share what they learned while creating the library and suggest how AI might help further in this field.
mathematical formalizationinteractive theorem proverLean 4game theorymechanism designsocial choicemachine-checked proofAI-assisted formalizationcomputational economicsmathlib
Authors
Xiaohui Bei, Jiajun Ma, Zhan Jing, Hongfei Fu, Zhihao Gavin Tang
Abstract
Mathematical formalization uses interactive theorem provers to turn informal mathematical statements into machine-checkable artifacts. The success of mathlib, a large collaborative library for Lean, illustrates the potential of this approach. Recent progress in AI-assisted programming and theorem proving is also making large-scale formalization more practical. This paper presents EconCSLib, an early Lean 4 library for computational economics, as both infrastructure and a case study for AI-assisted formalization. The library aims to provide reusable definitions and theorems for game theory, mechanism design, social choice, and related areas. Beyond verified proofs of existing results, the library also aims to host machine-checked open problems and formalization of modern research papers. We discuss the design principles behind the library, the lessons learned from its development, and future directions for AI-assisted formalization in computational economics.