pith. sign in

arxiv: 2606.13306 · v2 · pith:KFUD4QE7new · submitted 2026-06-11 · 💻 cs.GT

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

Nikhil Garg This is my paper

Pith reviewed 2026-07-03 23:53 UTC · model grok-4.3

classification 💻 cs.GT
keywords Lean formalizationAI-assisted verificationeconomics and computationformal methodsLean 4research paper formalizationhuman-AI workflowapplied modeling
0
0 comments X

The pith

A human-AI workflow lets economics researchers formalize their papers in Lean without knowing the language.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces EconCSLib, a Lean 4 library paired with an assisted workflow that lets researchers turn their economics and computation papers into formal statements and proofs. An LLM generates the Lean code, Lean checks the statements and proofs for correctness, and humans or LLM judges confirm that the formal version matches the original paper. The approach removes the need for researchers to learn Lean syntax or proof tactics themselves. The library already holds 20 fully formalized papers plus shared modules for probability, auctions, matching markets, and social choice, reaching nearly one million lines of code. If the workflow works as described, formalization could become a routine step in applied modeling research rather than a specialist task.

Core claim

The central claim is that a human-AI-Lean workflow enables researchers to formalize their own papers in Lean without knowing Lean. In this workflow an LLM writes the formal statements and proofs, Lean mechanically verifies them, and both human review and LLM-as-judge processes check that the translation preserves the paper's original claims. The library demonstrates the approach by containing 20 formalized papers together with reusable components for probability, stochastic processes, auctions, matching markets, social choice, and graph tools.

What carries the argument

The human-AI-Lean formalization workflow in which an LLM produces Lean code, Lean performs syntactic and semantic checks, and human or LLM judges audit fidelity to the source paper.

If this is right

  • Researchers without Lean expertise can still produce machine-checked versions of their models.
  • Shared libraries for auctions, matching, and probability become available for reuse across papers.
  • Systematic formalization of one's own publications can occur during the research process itself.
  • A growing public repository can accumulate verified statements from the economics and computation literature.
  • Agent skills, reporting dashboards, and auditing procedures can support scaling the workflow to more papers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same workflow pattern could be adapted for formalization tasks in other applied fields that use mathematical models.
  • Routine use might surface inconsistencies between informal descriptions and precise statements earlier in the publication cycle.
  • If the verification step catches translation errors reliably, it could serve as an additional check on the soundness of published economic models.

Load-bearing premise

LLM-generated Lean code that passes Lean checks and human or LLM review will reliably capture every important statement, assumption, and result from the original paper without omissions or additions.

What would settle it

A side-by-side comparison of one of the 20 formalized papers showing that its Lean version either omits a stated assumption or adds an unstated restriction that changes the paper's claimed result.

Figures

Figures reproduced from arXiv: 2606.13306 by Nikhil Garg.

Figure 1
Figure 1. Figure 1: Full paper statement dependency DAG for [ [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 1
Figure 1. Figure 1: Full paper statement dependency DAG for [ [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Screenshot of the paper-interface review dashboard for [ [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 2
Figure 2. Figure 2: Screenshot of the paper-interface review dashboard for [ [PITH_FULL_IMAGE:figures/full_fig_p007_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Full dependency DAG for [GHW01], Competitive Auctions and Digital Goods. The DAG shows the SODA paper. Section 8.2 is checked against the later journal version’s monotone-auction formulation of the revenue upper bound; the preliminary unrestricted wording is tracked only as source-version provenance. 36 [PITH_FULL_IMAGE:figures/full_fig_p036_3.png] view at source ↗
Figure 3
Figure 3. Figure 3: Full dependency DAG for [GHW01], Competitive Auctions and Digital Goods. The DAG shows the SODA paper. Section 8.2 is checked against the later journal version’s monotone-auction formulation of the revenue upper bound; the preliminary unrestricted wording is tracked only as source-version provenance. 23 [PITH_FULL_IMAGE:figures/full_fig_p023_3.png] view at source ↗
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.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents EconCSLib, a Lean 4 library and AI-assisted workflow for formalizing research papers in Economics & Computation. The central design is a human-AI-Lean loop in which LLMs generate code, Lean performs type-checking, and humans/LLM judges verify fidelity to the original statements. The public repository contains 20 fully formalized papers plus 4 partial ones (986k lines total) covering probability, auctions, matching, social choice, and graphs; the authors position this as an early systematic effort to formalize one's own publications while building a community resource.

Significance. If the workflow claim holds, the work would meaningfully lower barriers to formal verification in applied modeling fields by supplying both a large shared library of machine-checked statements and supporting tooling (agent skills, dashboards, auditing procedures). The scale of the artifact (nearly 1M lines of verified Lean code) and its public release constitute a concrete, reusable contribution that other researchers can build upon.

major comments (1)
  1. [Abstract] Abstract: The central claim that the workflow 'enable[s] researchers to formalize their papers in Lean without knowing Lean themselves' is load-bearing yet unsupported by evidence of non-author usage. The 20 formalized papers were produced by the authors themselves ('systematically pursue Lean formalization of one's own publications'); no external user studies, contribution logs from non-authors, pre/post Lean-knowledge assessments, or independent fidelity audits are referenced. Lean type-checking and LLM judges establish syntactic/proof correctness but do not by themselves demonstrate faithful capture of the original informal statements without omission or distortion.
minor comments (2)
  1. The paper would benefit from a short table or section listing the 20 formalized papers with brief descriptions of which components (definitions, theorems, proofs) were completed, to give readers a concrete sense of coverage.
  2. The GitHub repository URL and project webpage are given, but the manuscript does not indicate the current status of the review dashboard or auditing procedures (e.g., whether they are implemented and publicly usable).

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive feedback. We address the single major comment below and agree that the abstract claim requires qualification to reflect the current state of the project.

read point-by-point responses

  1. Referee: [Abstract] Abstract: The central claim that the workflow 'enable[s] researchers to formalize their papers in Lean without knowing Lean themselves' is load-bearing yet unsupported by evidence of non-author usage. The 20 formalized papers were produced by the authors themselves ('systematically pursue Lean formalization of one's own publications'); no external user studies, contribution logs from non-authors, pre/post Lean-knowledge assessments, or independent fidelity audits are referenced. Lean type-checking and LLM judges establish syntactic/proof correctness but do not by themselves demonstrate faithful capture of the original informal statements without omission or distortion.

    Authors: We agree that the claim is currently unsupported by external evidence. All 20 papers were formalized by the authors while developing the library, and no user studies, external logs, or independent audits exist at this stage. The workflow is explicitly designed around a human-AI-Lean loop in which domain researchers interact primarily through high-level guidance and verification rather than writing Lean code directly, with LLM generation, type-checking, and multi-stage auditing (human review plus LLM-as-judge) intended to preserve fidelity. We will revise the abstract to frame the workflow as one whose goal is to enable formalization without Lean expertise, while clarifying that the initial corpus was author-built and the public library now invites external contributions for broader validation. We will also expand the methods section to detail the auditing procedures used to check for omission or distortion. This is a partial revision because we cannot supply retrospective external usage data. revision: partial

Circularity Check

0 steps flagged

No circularity; paper presents library and workflow artifacts without derivations

full rationale

The paper contains no mathematical derivation chain, equations, predictions, or fitted parameters. Its contribution is the EconCSLib repository, shared libraries, and described human-AI-Lean workflow itself. No load-bearing claim reduces to a self-citation, self-definition, or input-by-construction; the 20 formalized papers are presented as outputs of the authors' own process, not as evidence of external non-expert use. This is a standard non-circular library paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

This is a software and workflow presentation paper; the central claim rests on the existence and usability of the library rather than mathematical derivations. No free parameters, invented entities, or non-standard axioms are introduced.

pith-pipeline@v0.9.1-grok · 5755 in / 1085 out tokens · 26090 ms · 2026-07-03T23:53:21.058348+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

30 extracted references · 2 canonical work pages

  1. [1]

    The paper-facing producer-fairness model, Theorems 3.1 and 3.2, Section 4 responsive-market definitions, and Appendix C responsive MSE decomposition are checked

    Human Verdict Formalized. The paper-facing producer-fairness model, Theorems 3.1 and 3.2, Section 4 responsive-market definitions, and Appendix C responsive MSE decomposition are checked. The strict variance-decrease endpoint is checked with the explicit interior-quality assumption 0 < q_v < 1 ; boundary audit rows at q_v = 0 and q_v = 1 record why the un...

  2. [2]

    • One-sentence recap: Theorems 3.1 and 3.2 are checked, with the strict variance-decrease endpoint carrying the explicit interior-quality additional assumption

    Closeout Status • Completion status: formalized. • One-sentence recap: Theorems 3.1 and 3.2 are checked, with the strict variance-decrease endpoint carrying the explicit interior-quality additional assumption. • Lean footprint: 680 paper-local Lean LOC; PaperInterface.lean is 332 lines; 27 human-review declarations are exposed. • Audit summary: paper cove...

  3. [3]

    Source and Scope • Paper: Balancing Producer Fairness and Efficiency via Prior-Weighted Rating System Design • Authors: Thomas Ma, Michael S. Bernstein, Ramesh Johari, and Nikhil Garg • Source version: ICWSM 2025 / arXiv:2207.04369 • Lean folder: MBJG25ProducerFairness/ • Human-facing theorem file: MBJG25ProducerFairness/PaperInterface.lean • Paper assumpt...

    work page arXiv 2025

  4. [4]

    • Theorem 3.1’s weak variance decrease, squared-bias nondecrease, and strict interior variance decrease are checked

    Researcher Summary of Checked Results • The posterior mean, bias, variance, squared-bias, individual-unfairness, Thompson-sampling, expected-regret, and responsive-MSE definitions are exposed as paper-facing formula rows. • Theorem 3.1’s weak variance decrease, squared-bias nondecrease, and strict interior variance decrease are checked. • Theorem 3.2’s sq...

  5. [5]

    Remaining Boundaries and Gaps None for the declared formalized paper surface. Human review remains partial as a review-process item: 10 of 27 rows have saved human entries, and two saved human entries are intentionally uncertain because they ask how to audit or trust shared-library predicates such as JensenConvex and GlobalMinAt

  6. [6]

    Boundary rows at q_v = 0 and q_v = 1 record why the unconditional strict statement is false at the endpoints

    Additional Assumptions Beyond Paper • Theorem 3.1 strict variance decrease: the formal statement assumes 0 < q_v < 1 . Boundary rows at q_v = 0 and q_v = 1 record why the unconditional strict statement is false at the endpoints. All other named assumptions are paper/model assumptions or paper theorem conditions: positive prior-shape mass, positive/nonnega...

  7. [7]

    The proof follows the algebraic structure of the paper’s fixed-model definitions

    Proof-Strategy Deviations None. The proof follows the algebraic structure of the paper’s fixed-model definitions. The strict-variance endpoint is a statement qualification, not a different proof strategy

  8. [8]

    Proof Tricks Worth Reusing • Add explicit boundary audit rows when a source strict inequality is only true on an interior domain. • Keep formula rows for definitions such as posterior mean, variance, and squared bias in PaperInterface.lean, so statement translation review is over paper formulas rather than opaque Lean helpers

  9. [9]

    At boundary qualities q_v = 0 and q_v = 1 , the variance term is identically zero, so strict decrease cannot hold unconditionally

    Mathematical Typos or Other Fixes Suggested in the Source Paper • Theorem 3.1 strict variance decrease: the unconditional strict wording should be read with the interior-quality condition 0 < q_v < 1 . At boundary qualities q_v = 0 and q_v = 1 , the variance term is identically zero, so strict decrease cannot hold unconditionally

  10. [10]

    The interior-quality condition for strict variance decrease is recorded above as an additional assumption, and the boundary behavior is exposed by separate audit rows

    Paper Issues or Caveats None. The interior-quality condition for strict variance decrease is recorded above as an additional assumption, and the boundary behavior is exposed by separate audit rows. ECONCSLIB 25 LMMS04 Fair Division Validation Report Final Validation Report: LMMS04 Fair Division Updated: 2026-07-02 Paper appendix note: this manuscript copy...

    2026

  11. [11]

    Sections 2 and 4 are checked, and Section 3 has the query, descent, Graham-consequence, rounded-search, and ratio-transfer support needed for the approximation route

    Human Verdict Partially formalized. Sections 2 and 4 are checked, and Section 3 has the query, descent, Graham-consequence, rounded-search, and ratio-transfer support needed for the approximation route. Full formalization still requires reusable fixed-dimension integer-programming runtime infrastructure for the PTAS/FPTAS layer. No fatal paper error is re...

  12. [12]

    • One-sentence recap: Sections 2 and 4 are fully formalized

    Closeout Status • Completion status: partially formalized. • One-sentence recap: Sections 2 and 4 are fully formalized. Section 3 has query/descent/rounded-search support. The PTAS/FPTAS runtime layer needs reusable fixed-dimension IP complexity infrastructure. • Lean footprint: 80,496 paper-local Lean LOC; PaperInterface.lean is 303 lines; 48 human-revie...

  13. [13]

    Source and Scope • Paper: On Approximately Fair Allocations of Indivisible Goods • Authors: Richard J. Lipton, Evangelos Markakis, Elchanan Mossel, and Amin Saberi • Source version: ACM EC 2004, DOI 10.1145/988772.988792 • Lean folder: LMMS04FairDivision/ • Human-facing theorem file: LMMS04FairDivision/PaperInterface.lean • Paper assumption file: LMMS04Fa...

    work page doi:10.1145/988772.988792 2004

  14. [14]

    Researcher Summary of Checked Results • Section 2 finite-allocation envy definitions, envy-cycle reduction, bounded-envy allocation, and the real-interval atom-bound route are checked. • Section 3 has checked adaptive-query lower-bound wrappers, Graham-scheduling consequence rows, rounded type/value-pair search infrastructure, bounded-optimal allocation s...

  15. [15]

    The current Lean code records that layer through explicit partial-boundary rows and proves the supporting finite algebraic, rounded-search, and transfer statements around it

    Remaining Boundaries and Gaps Full formalization requires reusable fixed-dimension integer-programming runtime infrastructure for the PTAS/FPTAS layer in Theorem 3.3. The current Lean code records that layer through explicit partial-boundary rows and proves the supporting finite algebraic, rounded-search, and transfer statements around it

  16. [16]

    Additional Assumptions Beyond Paper None. Positive error parameters, finite duplicate-free goods enumerations, positive atom bounds, normalized random- allocation weights, and Section 3 load and rounding conditions are source theorem/model conditions. Graham schedul- ing and fixed-dimension IP runtime are partial or external theorem/library boundaries, no...

  17. [17]

    • Claim 3.4 required a more explicit finite-descent proof than the prose presentation

    Proof-Strategy Deviations • Theorem 4.1 is proved with a smaller finite counterexample than the source exposition; this is sufficient for the impossibility theorem. • Claim 3.4 required a more explicit finite-descent proof than the prose presentation. The formal proof separates high-source moves from low-only tie-breaking moves. • Theorem 4.2 is recorded a...

  18. [18]

    • For prose partition arguments over intervals, formalize the constructive endpoint choice explicitly; this exposes min/max or supremum direction errors cleanly

    Proof Tricks Worth Reusing • For algorithmic PTAS/FPTAS claims, isolate the finite algebraic/search support from the machine-level runtime theorem so the partial boundary is precise. • For prose partition arguments over intervals, formalize the constructive endpoint choice explicitly; this exposes min/max or supremum direction errors cleanly

  19. [19]

    To obtain progress and the stated finite partition, this should be read as a maximal/supremal endpoint choice

    Mathematical Typos or Other Fixes Suggested in the Source Paper • Lemma 2.4 proof typo: the prose appears to say to choose the minimum endpoint whose prefix interval has value at most alpha for every player. To obtain progress and the stated finite partition, this should be read as a maximal/supremal endpoint choice

  20. [20]

    The Lemma 2.4 endpoint issue is recorded as a typo, not a caveat

    Paper Issues or Caveats No fatal paper error is reported. The Lemma 2.4 endpoint issue is recorded as a typo, not a caveat. Several implicit real-support and atom-bound modeling choices are documented in the evidence below. The paper status is partial only because the reusable fixed-dimension IP runtime infrastructure for the final PTAS/FPTAS layer is not...

    2026

  21. [21]

    Human Verdict Partially formalized. The finite auction model, generalized Vickrey auction, single-minded welfare/set-packing re- ductions, greedy approximation, critical-value lemmas, and average-greedy truthfulness theorem are checked. Full formalization still requires reusable computational-complexity infrastructure for the native Theorem 6.1 hardness a...

  22. [22]

    • One-sentence recap: Greedy approximation, truthfulness, and Theorem 6.1 reductions are formalized

    Closeout Status • Completion status: partially formalized. • One-sentence recap: Greedy approximation, truthfulness, and Theorem 6.1 reductions are formalized. Full formalization requires computational complexity results that are out of scope. • Lean footprint: 7,582 paper-local Lean LOC; PaperInterface.lean is 371 lines; 39 human-review declarations are ...

    2026

  23. [23]

    Source and Scope • Paper: Truth Revelation in Approximately Efficient Combinatorial Auctions • Authors: Daniel Lehmann, Liadan Ita O’Callaghan, and Yoav Shoham • Source version: Journal of the ACM 49(5), 2002 • Lean folder: LOS02CombinatorialAuctions/ • Human-facing theorem file: LOS02CombinatorialAuctions/PaperInterface.lean • Paper assumption file: LOS02...

    2002

  24. [24]

    • The generalized Vickrey auction truthfulness theorem and nonnegative truthful-utility proposition are checked for the finite combinatorial-auction model

    Researcher Summary of Checked Results • The finite combinatorial-auction definitions are checked with source-facing formula rows for utility, truthful- ness, generalized Vickrey payments, single-minded profiles, set-packing value, greedy order, accepted set, and payments. • The generalized Vickrey auction truthfulness theorem and nonnegative truthful-util...

  25. [25]

    The current Lean code proves the finite auction/reduction statements and records the complexity consequences as conditional external-boundary interfaces

    Remaining Boundaries and Gaps Full formalization requires reusable computational-complexity infrastructure for the final native Theorem 6.1 hardness and NP = ZPP consequences. The current Lean code proves the finite auction/reduction statements and records the complexity consequences as conditional external-boundary interfaces

  26. [26]

    Additional Assumptions Beyond Paper None. The nonnegative/nonempty single-minded domain, optimal-allocation comparison conditions, denied-bidder case, nonnegative-value deviation domain, critical-value conditions, and finite-threshold condition are source theorem conditions. The two complexity rows are partial boundaries, not additional assumptions accept...

  27. [27]

    The finite auction, greedy, and critical-value arguments follow the paper’s proof routes; the native complexity consequences are not claimed as fully formalized

    Proof-Strategy Deviations None beyond the formalization boundaries already recorded above. The finite auction, greedy, and critical-value arguments follow the paper’s proof routes; the native complexity consequences are not claimed as fully formalized

  28. [28]

    This keeps the judged review surface at the paper-formula level rather than at opaque Lean function signatures

    Proof Tricks Worth Reusing • For source definitions that otherwise appear as opaque function abbreviations, expose exact formula or iff rows in PaperInterface.lean before running LLM-as-judge translation. This keeps the judged review surface at the paper-formula level rather than at opaque Lean function signatures. • For partial complexity results, separa...

  29. [29]

    Mathematical Typos or Other Fixes Suggested in the Source Paper None found

  30. [30]

    The paper status is partial only because the reusable computational- complexity infrastructure for the final native complexity claims is not yet present in the library

    Paper Issues or Caveats No auction-theoretic paper error is reported. The paper status is partial only because the reusable computational- complexity infrastructure for the final native complexity claims is not yet present in the library. ECONCSLIB 29