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.

翻译：数学形式化利用交互式定理证明器将非正式的数学陈述转化为机器可验证的物件。mathlib（一个大型协作式Lean库）的成功展示了这种方法的潜力。近期人工智能辅助编程与定理证明的进展也使得大规模形式化变得更加可行。本文介绍了EconCSLib——一个用于计算经济学的早期Lean 4库，它既是基础设施，也是AI辅助形式化的案例研究。该库旨在为博弈论、机制设计、社会选择及相关领域提供可复用的定义和定理。除了对现有结果进行验证性证明外，该库还致力于托管经机器验证的开放问题以及现代研究论文的形式化。我们讨论了该库的设计原则、开发过程中的经验教训，以及AI辅助形式化在计算经济学中的未来方向。