Contribute
Interested in contributing or formalizing your own paper?
To get started in formalizing your own paper, clone the repository and open an LLM agent tool (I use Codex with a high-reasoning configuration). Give the agent the paper link, and ask it to formalize the paper using the skill and workflow in the repository. (And please let me know what your experience is like).
New paper formalizations should start in a private workflow and be proposed to enter the library through a pull request when ready. For questions or contributions, contact ngarg@cornell.edu.
Library: reusable components
The shared library contains paper-independent Lean infrastructure that current paper formalizations reuse.
| Component | Content details | Lines of code |
|---|---|---|
| Foundations: finite math and graph tools | Core finite mathematics used across the formalizations: finite-choice distances, ranking and order conversions, finite-sum algebra, threshold and interval certificates, asymptotic estimates, and graph-cycle extraction for local-improvement arguments. | 15,970 |
| Foundations: probability and stochastic processes | Probability infrastructure for recommendation, ratings, pricing, and ranking papers: finite PMFs and expectations, conditional kernels, Gaussian and random-utility comparisons, large-deviation and method-of-types certificates, stochastic dominance, order statistics, Markov chains, MDPs, CTMCs, Poisson processes, and renewal-reward models. | 76,470 |
| Foundations: optimization, certificates, and complexity | Certificate-oriented optimization and complexity for paper-level endpoints: argmax, endpoint, and bisection principles; finite-search and output-check certificates; approximation and LP witnesses; binary-policy games; move-graph descent; strategic and choice equilibria; NP/ZPP consequence interfaces; and Yao-style lower-bound certificates. | 5,371 |
| Social choice, rankings, voting, and fair division | Executable social-choice infrastructure: ranked ballots, next-active support counts, RCV/STV traces, quotas, coalition-safety lemmas, final-order structures, candidate-deletion reductions, Thiele-style proportionality, Mallows/Kendall ranking models, payoff interfaces, envy graphs, bounded-envy algorithms, and indivisible-goods fairness statements. | 27,894 |
| Auctions and mechanisms | Mechanism-design infrastructure for digital-goods, combinatorial, and position auctions: allocation and payment semantics, utility formulas, DSIC truthfulness, VCG-style welfare maximization, benchmark-competitive auctions, single-minded set packing, greedy mechanisms, and critical-value certificates. | 12,881 |
| Online algorithms and regret | Online allocation infrastructure centered on AdWords and platform learning: matching/allocation state machines, primal-dual accounting, competitive-ratio certificates, regret interfaces, and hooks for randomized lower-bound arguments. | 4,374 |
| Matching markets and admissions | Stable matching and admissions infrastructure: one-to-one and many-to-one assignments, blocking-pair stability, deferred-acceptance invariants, applicant/proposer optimality, quota admissions, strategic application cutoffs and payoffs, and two-group policy objective comparisons. | 3,924 |
| Ratings and recommender systems | Ratings and recommendation infrastructure: Bayesian binary and ordinal signal models, posterior-mean rating formulas, prior-weighted updates, monotonicity and correction lemmas, Thompson-sampling entrypoints, exposure/allocation policies, classwise fairness constraints, top-k recommendation surfaces, policy averaging, and accuracy/diversity trade-off statements. | 3,186 |
Current status
The public repository currently contains formalized papers and selected public partial formalizations whose remaining assumptions are explicit. Human review refers to a human certifying that a Lean statement exactly corresponds to a paper statement. This is augmented with substantial LLM-as-judge checks run for every public paper, including for coverage of paper results, matches, and holistic audits that statements match.
| Paper | Status | Human review | Lines of Code | Note |
|---|---|---|---|---|
| College Admissions and the Stability of Marriage by D. Gale and L. S. Shapley; American Mathematical Monthly, 1962. | 0/7 reviewed | 388 | This only uses a few lines of code as its infrastructure has largely been elevated to the shared matching library. | |
| The Economics of Matching: Stability and Incentives by Alvin E. Roth; Mathematics of Operations Research, 1982. | 0/29 reviewed | 8,931 | ||
| Competitive Auctions and Digital Goods by Andrew V. Goldberg, Jason D. Hartline, and Andrew Wright; SODA, 2001. | 0/30 reviewed | 14,624 | Formalizes the SODA paper; Theorem 8.2 uses the refined monotone-auction wording from the journal version Goldberg-Hartline-Karlin-Saks-Wright 2006. | |
| AdWords and Generalized Online Matching by Aranyak Mehta, Amin Saberi, Umesh Vazirani, and Vijay V. Vazirani; Journal of the ACM, 2007. | 0/43 reviewed | 13,741 | ||
| Internet Advertising and the Generalized Second-Price Auction by Benjamin Edelman, Michael Ostrovsky, and Michael Schwarz; American Economic Review, 2007. | 0/26 reviewed | 133,338 | ||
| Designing Optimal Binary Rating Systems by Nikhil Garg, Ramesh Johari; AISTATS / PMLR 89, 2019. | 0/55 reviewed | 85,832 | ||
| Who is in Your Top Three? Optimizing Learning in Elections with Many Candidates by Nikhil Garg, Lodewijk Gelauff, Sukolsak Sakshuwong, Ashish Goel; HCOMP, 2019. | 0/17 reviewed | 35,059 | ||
| Designing Informative Rating Systems: Evidence from an Online Labor Market by Nikhil Garg, Ramesh Johari; Manufacturing & Service Operations Management 23(3), 2020. | 0/15 reviewed | 7,044 | ||
| Algorithmic Monoculture and Social Welfare by Jon Kleinberg and Manish Raghavan; PNAS, 2021. | 0/49 reviewed | 65,666 | ||
| Test-optional Policies: Overcoming Strategic Behavior and Informational Gaps by Zhi Liu and Nikhil Garg; EAAMO, 2021. | 0/23 reviewed | 125,744 | ||
| Driver Surge Pricing by Nikhil Garg and Hamid Nazerzadeh; Management Science, 2022. | 0/36 reviewed | 142,959 | ||
| Optimal Strategies in Ranked-Choice Voting by Sanyukta Deshpande; Nikhil Garg; Sheldon H. Jacobson; arXiv:2407.13661, 2024; working paper. | 0/65 reviewed | 54,427 | ||
| Reconciling the Accuracy-Diversity Trade-off in Recommendations by Kenny Peng, Manish Raghavan, Emma Pierson, Jon Kleinberg, and Nikhil Garg; The ACM Web Conference, 2024. | 0/42 reviewed | 52,018 | Proposition 2's printed finite bound appears to miss a factor of 2; Lean proves the corrected finite bound, which is sufficient for the asymptotic 1/2-homogeneity result. | |
| User-item fairness tradeoffs in recommendations by Sophie Greenwood, Sudalakshmee Chiniah, and Nikhil Garg; NeurIPS, 2024. | 0/48 reviewed | 46,186 | ||
| A No Free Lunch Theorem for Human-AI Collaboration by Kenny Peng, Nikhil Garg, Jon Kleinberg; AAAI, 2025. | 0/15 reviewed | 2,032 | ||
| Addressing Discretization-Induced Bias in Demographic Prediction by Evan Dong, Aaron Schein, Yixin Wang, and Nikhil Garg; PNAS Nexus, 2025. | 0/41 reviewed | 26,133 | ||
| Balancing Producer Fairness and Efficiency via Prior-Weighted Rating System Design by Thomas Ma, Michael S. Bernstein, Ramesh Johari, and Nikhil Garg; ICWSM, 2025. | 10/27 reviewed; 2 uncertain | 680 | Strict variance decrease is formalized with the explicit interior-quality assumption 0 < q_v < 1. | |
| Capacity Constraints Make Admissions Processes Less Predictable by Evan Dong; Nikhil Garg; Sarah Dean; AAAI-26 published version, DOI 10.1609/aaai.v40i45.41179. | 0/66 reviewed | 11,553 | ||
| Combatting Gerrymandering with Ranked Choice Voting: an Experimental Analysis of Multi-member Districts in the United States by Nikhil Garg; Wes Gurnee; David Rothschild; David Shmoys; Operations Research, 2026, DOI 10.1287/opre.2024.1167. | 0/19 reviewed | 9,398 | ||
| Simpler Than You Think: The Practical Dynamics of Ranked Choice Voting by Sanyukta Deshpande; Nikhil Garg; Sheldon H. Jacobson; Journal of Computational Social Science, 2026. | 0/50 reviewed | 20,752 | ||
| Truth Revelation in Approximately Efficient Combinatorial Auctions by Daniel Lehmann, Liadan Ita O'Callaghan, and Yoav Shoham; Journal of the ACM, 2002. | 0/39 reviewed | 7,582 | Greedy approximation, truthfulness, and Theorem 6.1 reductions are formalized. Full formalization requires computational complexity results that are out of scope. | |
| On Approximately Fair Allocations of Indivisible Goods by Richard J. Lipton, Evangelos Markakis, Elchanan Mossel, and Amin Saberi; ACM EC, 2004. | 0/44 reviewed | 80,496 | 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. | |
| Iterative Local Voting for Collective Decision-making in Continuous Spaces by Nikhil Garg; Vijay Kamble; Ashish Goel; David Marn; Kamesh Munagala; JAIR 64, 2019. | 0/47 reviewed | 23,490 | Full formalization requires proving stochastic subgradient descent convergence. Theorem 3 is proved as a constrained alternative in general and as the original statement under the explicit full-space condition. | |
| Quantifying Spatial Under-reporting Disparities in Resident Crowdsourcing by Zhi Liu, Uma Bhandaram, Nikhil Garg; Nature Computational Science, 2024. | 0/25 reviewed | 18,557 | Full formalization requires a homogeneous Poisson process and stopping-time derivation. |