This paper presents EconCSLib, a Lean 4 library and workflow for formalizing research papers in Economics and Computation with language-model assistance. The central design principle is a human-AI-Lean workflow: an LLM writes Lean code, Lean checks formal statements and proofs, and humans (assisted by an LLM) verify the translation boundary from paper claims to formal statements. EconCSLib is organized around research papers, preserving their formal statements and following their proof structure to the extent possible; reusable mathematical statements are elevated into shared EconCS infrastructure. The workflow is designed to be author-facing: researchers can formalize their own papers, inspect the Lean code's translations of paper-facing statements, and contribute reusable components back to the library; this is supported by post-formalization validation reports, paper result dependency graphs, and a review dashboard. The current public repository contains 11 formalized papers and 3 partially formalized papers, along with initial libraries for probability, auctions, matching markets, and graph tools. The library and workflow are available at https://github.com/nikhgarg/EconCSLib, with corresponding project webpage at https://gargnikhil.com/EconCSLib/. To our knowledge, we are also among the first applied math researchers to systematically pursue Lean formalization of one's own publications in the process of building such a community library. We welcome users and contributors to the project.

翻译：本文介绍了EconCSLib，一个基于Lean 4的库与工作流，旨在通过语言模型辅助实现经济学与计算研究论文的形式化。核心设计原则为人机-AI-Lean协作工作流：大语言模型编写Lean代码，Lean检验形式化陈述与证明，而人类（借助大语言模型辅助）验证从论文主张到形式化陈述的翻译边界。EconCSLib以研究论文为核心组织框架，保留其形式化陈述并尽可能遵循原始证明结构；可复用的数理表述被提升为共享的EconCS基础设施。该工作流面向作者：研究者可对其自身论文进行形式化，审查Lean代码对论文级陈述的翻译，并向库中贡献可复用组件；这一过程由形式化后验证报告、论文结果依赖关系图及评审看板提供支持。当前公开仓库包含11篇完全形式化论文和3篇部分形式化论文，以及概率论、拍卖、匹配市场和图工具的基础库。该库与工作流可通过https://github.com/nikhgarg/EconCSLib 获取，对应项目网页为https://gargnikhil.com/EconCSLib/。据我们所知，在构建此类社区库的过程中，我们也是首批系统性地对自身出版物进行Lean形式化的应用数学研究者之一。我们欢迎用户与贡献者加入该项目。