EconCSLib: AI-Assisted Lean Formalization for Economics & Computation research
Pith reviewed 2026-06-27 05:09 UTC · model grok-4.3
The pith
A human-AI-Lean workflow lets researchers formalize their Economics and Computation papers.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
EconCSLib organizes formalizations around individual research papers, preserving their statements and proof structures to the extent possible while moving reusable mathematical statements into shared infrastructure. The workflow combines LLM code generation, Lean verification of statements and proofs, and human oversight specifically at the boundary where paper claims are translated into formal statements. The library is designed to be author-facing, with tools such as post-formalization validation reports, paper result dependency graphs, and a review dashboard to support researchers formalizing their own work.
What carries the argument
The human-AI-Lean workflow in which an LLM writes Lean code, Lean checks formal statements and proofs, and humans verify the translation boundary from paper claims to formal statements.
If this is right
- Researchers can formalize their own papers, inspect the Lean translations of paper-facing statements, and contribute reusable components back to the library.
- Initial shared libraries for probability, auctions, matching markets, and graph tools become available for reuse across papers.
- Post-formalization validation reports, paper result dependency graphs, and a review dashboard assist the formalization process.
- The library grows through author contributions of both paper-specific formalizations and reusable infrastructure.
Where Pith is reading between the lines
- Formal statements produced this way could serve as stable reference points when comparing models across different papers.
- The same workflow structure might apply to formalization efforts in other applied fields that rely on similar combinations of probability and optimization.
- If LLM translation accuracy improves, the human review step could eventually focus on fewer, higher-level checks.
Load-bearing premise
Humans can reliably detect when an LLM-generated Lean statement fails to capture the original paper's intended meaning or introduces subtle errors in economic modeling assumptions.
What would settle it
A case in which an LLM-generated formalization passes both Lean checks and human review, yet later independent analysis shows that a key modeling assumption from the source paper was altered or omitted.
Figures
read the original abstract
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/.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper describes EconCSLib, a Lean 4 library and associated workflow for formalizing papers in Economics and Computation using AI assistance. The workflow consists of an LLM generating Lean code, Lean verifying the statements and proofs, and humans verifying that the formal statements accurately reflect the original paper claims. The library is structured around individual papers with reusable components extracted to shared libraries. It currently includes 11 formalized papers and 3 partially formalized ones, with libraries for probability, auctions, matching markets, and graph tools. The project is open source and author-facing, with tools for validation reports and dependency graphs.
Significance. If effective, this work could significantly advance the formal verification of results in the Economics and Computation community by providing machine-checked proofs and reusable formal statements. The concrete achievement of formalizing 11 papers using the described workflow, along with the public repository, demonstrates feasibility and provides a foundation for community contributions. This is particularly valuable as it involves researchers formalizing their own publications, which helps ensure fidelity to the original claims.
major comments (1)
- [Abstract] The abstract reports the number of formalized papers (11) and partially formalized (3) but does not include any metrics or evidence on the correctness of these formalizations, such as the proportion of theorems formalized per paper or any reported discrepancies found during human verification. This information is load-bearing for assessing whether the workflow reliably captures paper claims.
minor comments (2)
- Consider adding a brief example in the main text of a paper statement and its Lean formalization to illustrate the translation boundary verification step.
- [Abstract] The phrase 'to our knowledge, we are also among the first' could be clarified with more context on prior efforts in formalizing applied math papers.
Simulated Author's Rebuttal
We thank the referee for the positive evaluation and the constructive comment on the abstract. We address it directly below.
read point-by-point responses
-
Referee: [Abstract] The abstract reports the number of formalized papers (11) and partially formalized (3) but does not include any metrics or evidence on the correctness of these formalizations, such as the proportion of theorems formalized per paper or any reported discrepancies found during human verification. This information is load-bearing for assessing whether the workflow reliably captures paper claims.
Authors: We agree that the abstract would be strengthened by additional context on verification. The described workflow includes an explicit human verification step (assisted by LLM) to confirm that formal statements accurately reflect the original paper claims, with any discrepancies resolved before inclusion. However, the library does not collect or report quantitative per-paper metrics such as 'proportion of theorems formalized' because formalization targets key results and reusable components rather than exhaustive coverage of every theorem in a paper; the structure is paper-centric by design. In the revised version we will update the abstract to note that every formalized paper has undergone human verification for fidelity to the source claims. Detailed per-paper validation reports and dependency information remain available in the public repository. revision: yes
Circularity Check
No significant circularity
full rationale
The paper is a descriptive account of a Lean library and human-AI workflow for formalizing economics papers. It contains no derivations, equations, predictions, fitted parameters, or load-bearing claims that could reduce to self-definition, self-citation chains, or renaming of known results. The central content is a process description plus concrete deliverables (11 formalized papers, shared libraries), which are externally verifiable outputs rather than internally circular reasoning. No steps meet the criteria for circularity.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.