EconCSLib (Nikhil Garg): AI-assisted paper formalization

Research applicability

Lean 4 library and AI-assisted workflow for formalizing economics and computation research papers, with agent skills and human-facing validation reports.

Getting started

Read the repository quickstart and inspect a paper folder validation report and PaperInterface.lean before adapting the documented workflow.

Maintenance

Future maintenance not established by this source review.

License

Licence not independently audited; check source terms before reuse.

Workflow & human oversight

Workflow level unspecified for this resource; researchers define objectives, control input data and validate outputs. Suggested adoption steps were not exercised.

Workflow level is not an evidence score; higher is not better evidence.

Approach

An LLM writes Lean code, Lean checks statements and proofs, and translation audits assess correspondence with the source paper; the repository documents reports and paper interfaces for inspection.

Limitations

Paper extract and repository documentation only; no Lean build or proof audit executed. Lean checks formal statements under assumptions, not whether translation captures the original paper. Reported library size/completion is not independently checked; model access and costs vary.

Reproducibility

Primary documentation reviewed on 2026-10-17. No software, model outputs or reported results independently reproduced.

Adoption requirements

Lean/mathlib/CSLib toolchain, an LLM coding agent and source papers; repository specifies v4.30.0-rc2 at retrieval. Domain expertise remains necessary to inspect assumptions and translation fidelity.