EconCSLib uses LLMs to formalize EconCS papers in Lean 4

Nikhil Garg has released EconCSLib, a Lean 4 library and workflow designed to formalize research papers in Economics and Computation with the help of large language models. The core principle is a human-AI-Lean loop: an LLM writes Lean code that encodes formal statements and proofs; Lean itself checks their correctness; and humans, assisted by the LLM, verify that the formal statements accurately translate the paper's claims. This tripartite approach aims to reduce the burden of manual formalization while maintaining rigor. The library is structured around individual papers, preserving their formal statements and following their proof structures as closely as possible, with reusable mathematical components promoted into shared infrastructure.

Currently, the repository contains 11 fully formalized papers and 3 partially formalized ones, along with initial libraries for probability, auctions, matching markets, and graph tools. The workflow is author-facing: researchers can formalize their own publications, inspect how Lean code translates their paper's statements, and contribute reusable components back to the library. Additional features include post-formalization validation reports, dependency graphs for paper results, and a review dashboard. Accepted to the EC'26 Workshop on AI-Driven Research in EconCS, EconCSLib is positioned as one of the early systematic efforts by applied math researchers to formalize their own publications while building a community library.