# EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research

arXiv: https://arxiv.org/abs/2606.13306 · HTML: https://mlsanity.com/paper/2606.13306/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 Jun 2026.

## Built on by (most cited first, 7 of 7)

- [Prove2Me: An Open Collaborative Platform for Scaling Math Formalization](https://mlsanity.com/paper/2608.28433/) (2026)
- [CausalSmith: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference](https://mlsanity.com/paper/2607.22511/) (2026)
- [AI with Authority, from Application to Silicon](https://mlsanity.com/paper/2608.21356/) (2026)
- [GenLimitLib: A Formal Library for Language Generation in the Limit and AI-Assisted Mathematical Research](https://mlsanity.com/paper/2609.36663/) (2026)
- [Co-Linguistics: AI-augmented Theory Construction in Linguistics](https://mlsanity.com/paper/2609.37635/) (2026)
- [A Testable Theory of Atomic Features](https://mlsanity.com/paper/2610.05794/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

This paper presents EconCSLib, a Lean 4 library and workflow for formalizing research papers in applied modeling fields such as Economics and Computation, with language-model assistance. The goal of EconCSLib is to enable researchers to formalize their papers in Lean without knowing Lean themselves. The central design principle is a human-AI-Lean formalization workflow: an LLM writes Lean code, Lean checks formal statements and proofs, and both humans and LLM-as-judge processes can verify that the paper's statements were translated into Lean correctly. We develop agent skills, human-facing reporting, a review dashboard, and auditing procedures to support this workflow. The current public repository contains 20 formalized papers and 4 partially formalized papers, along with shared libraries for probability (including stochastic processes), auctions, matching markets, social choice, and graph tools, totaling 986,391 lines of Lean code. 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. The library and workflow are available at https://github.com/nikhgarg/EconCSLib, with corresponding project webpage at https://gargnikhil.com/EconCSLib/.