Applied Modeling Lib

Library

Reusable components

The shared library separates mathematical foundations, research-area tools, and application-specific models. The table summarizes the main concepts covered; each area links to its Lean entry point.

Area	Content	Lines of code
Foundations: mathematics and discrete structures	Fixed-point theorems; convexity and finite-dimensional geometry; graphs, combinatorics, and counting; asymptotic analysis; Boolean circuits.	54,640
Foundations: probability and stochastic processes	Concentration and large deviations; coupling and Wasserstein distance; conditional laws and Bayesian updating; order statistics; Markov chains, martingales, Poisson and renewal processes.	195,504
Foundations: optimization	Convex optimization and duality; gradient, subgradient, and mirror descent; stochastic optimization; proximal maps and projections; argmax stability and envelope theorems.	19,997
AI and applications	Alignment axioms and welfare; differential privacy and composition; algorithmic fairness; admissions policies; rating systems; recommender systems and producer/user fairness.	26,366
Learning and statistics	Generalization and sample complexity; calibration, multiaccuracy, and omniprediction; online learning and regret; bandits; reinforcement learning; preference learning and human feedback.	59,476
Algorithms and complexity	Online allocation and advertising; competitive analysis and regret reductions; primal-dual approximation arguments; computational complexity, reductions, and neural-network verification.	5,047
Game theory	Best responses and Nash equilibrium; preference games; threshold strategies; multitask incentives; performative prediction and strategic responses.	27,323
Markets and matching	Stable and many-to-one matching; deferred acceptance and proposer optimality; continuum markets and admission cutoffs; manipulation and blocking; public decisions.	10,958
Mechanism design and auctions	Incentive compatibility, truthfulness, and payments; VCG and generalized second-price auctions; position, digital-goods, and combinatorial auctions; welfare and revenue.	12,942
Social choice and fair division	Preference rankings and aggregation; ranked-choice voting and proportionality; indivisible goods and chores; bounded envy and envy freeness up to any item (EFX); Pareto efficiency.	31,379
Queueing	Single-server and many-server queues; priority service and processor sharing; waiting times, workloads, and stationary distributions; heavy-traffic limits; congestion externalities and pricing.	151,201

Papers

Current formalizations

Formalized means the selected Lean statements have checked proofs; reports explain their correspondence to the paper. Partially formalized marks unfinished developments. Formalization gap notes flag substantial extra assumptions, simplifications, or missing conclusions in the current formalization.

Human review shows how many paper-to-Lean statement comparisons a human has reviewed, out of the selected results. Automated comparisons and independent agent audits provide additional checks; they do not count as human review.

Paper	Status	Human review	Lines of Code	Notes
College Admissions and the Stability of Marriage by D. Gale and L. S. Shapley; American Mathematical Monthly, 1962.	Formalized	0/6	5,467	Report Lean statements Dependency map Review packet Repo
The Regulation of Queue Size by Levying Tolls by P. Naor; Econometrica 37(1), 1969.	Formalized	0/6	922	Report Lean statements Dependency map Review packet Repo Few lines of code as much of machinery is in the shared library
The Economics of Matching: Stability and Incentives by Alvin E. Roth; Mathematics of Operations Research, 1982.	Formalized	0/10	11,294	Report Lean statements Dependency map Review packet Repo
Optimal Incentive-Compatible Priority Pricing for the M/M/1 Queue by Haim Mendelson and Seungjin Whang; Operations Research 38(5), 1990.	Formalized	0/5	3,616	Report Lean statements Dependency map Review packet Repo Few lines of code as much of machinery is in the shared library
A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting by Yoav Freund and Robert E. Schapire; Journal of Computer and System Sciences 55(1):119–139, 1997.	Formalized	0/14	1,136	Report Lean statements Dependency map Review packet Repo Few lines of code as much of machinery is in the shared library
Competitive Auctions and Digital Goods by Andrew V. Goldberg, Jason D. Hartline, and Andrew Wright; SODA, 2001.	Formalized	0/12	24,842	Report Lean statements Dependency map Review packet Repo Formalizes the SODA paper; Theorem 8.2 uses the refined monotone-auction wording from the journal version. Formalization gap: Lemma 8.1 and Theorem 8.2 are proved for finite offer support; continuous-offer cases remain unproved 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.	Formalized	0/50	22,118	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 8's limit is proved when its finite-error term vanishes; deriving that condition from the paper's small-bid regime remains unproved.
Internet Advertising and the Generalized Second-Price Auction by Benjamin Edelman, Michael Ostrovsky, and Michael Schwarz; American Economic Review, 2007.	Formalized	0/13	142,501	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 8 uniqueness is proved among common symmetric continuation plans; uniqueness among arbitrary bidder-specific plans remains unproved.
Maxing and Ranking with Few Assumptions by Moein Falahatgar, Yi Hao, Alon Orlitsky, Venkatadheeraj Pichapati, and Vaishakh Ravindrakumar; NeurIPS, 2017.	Formalized	0/23	33,818	Report Lean statements Dependency map Review packet Repo
Designing Optimal Binary Rating Systems by Nikhil Garg, Ramesh Johari; AISTATS / PMLR 89, 2019.	Formalized	0/33	96,123	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 3.1 is proved for optimization of its displayed rate formula for at least three levels; identifying that formula with the actual ranking-quality exponent and proving Lemma C.4's same-objective equivalence remain unproved.
Fundamental Limits of Testing the Independence of Irrelevant Alternatives in Discrete Choice by Arjun Seshadri and Johan Ugander; ACM EC 2019; arXiv version (2020).	Formalized	0/11	10,986	Report Lean statements Dependency map Review packet Repo
Iterative Local Voting for Collective Decision-making in Continuous Spaces by Nikhil Garg; Vijay Kamble; Ashish Goel; David Marn; Kamesh Munagala; JAIR 64, 2019.	Formalized	0/12	54,809	Report Lean statements Dependency map Review packet Repo Theorem 3 is proved as a constrained alternative in general and as the original statement under the explicit full-space condition.
Who is in Your Top Three? Optimizing Learning in Elections with Many Candidates by Nikhil Garg; Lodewijk Gelauff; Sukolsak Sakshuwong; Ashish Goel; HCOMP, 2019.	Formalized	0/15	38,678	Report Lean statements Dependency map Review packet Repo
Axioms for Learning from Pairwise Comparisons by Ritesh Noothigattu, Dominik Peters, and Ariel D. Procaccia; NeurIPS, 2020.	Formalized	0/10	2,507	Report Lean statements Dependency map Review packet Repo
Designing Informative Rating Systems: Evidence from an Online Labor Market by Nikhil Garg, Ramesh Johari; Manufacturing & Service Operations Management 23(3), 2020.	Formalized	0/3	9,718	Report Lean statements Dependency map Review packet Repo
Performative Prediction by Juan C. Perdomo, Tijana Zrnic, Celestine Mendler-Dünner, and Moritz Hardt; ICML, 2020.	Formalized	0/11	3,813	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 3.10 gives eventual high-probability containment in dimension > 2 with uniform moments and stronger regularity; the printed sample-count and burn-in bounds remain unproved.
Algorithmic Monoculture and Social Welfare by Jon Kleinberg and Manish Raghavan; PNAS, 2021.	Formalized	0/49	116,134	Report Lean statements Dependency map Review packet Repo
Test-optional Policies: Overcoming Strategic Behavior and Informational Gaps by Zhi Liu and Nikhil Garg; EAAMO, 2021.	Formalized	0/15	210,358	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 3.1 assumes stability against profitable group entry; voluntary Lemma 4.1 assumes maximal participation. Deriving these refinements from the paper’s equilibrium definition remains unproved.
An Algorithmic Framework for Bias Bounties by Ira Globus-Harris, Michael Kearns, and Aaron Roth; ACM FAccT, 2022.	Formalized	0/15	14,755	Report Lean statements Dependency map Review packet Repo
Driver Surge Pricing by Nikhil Garg and Hamid Nazerzadeh; Management Science, 2022.	Formalized	0/16	203,502	Report Lean statements Dependency map Review packet Repo
Supply-Side Equilibria in Recommender Systems by Meena Jagadeesan, Nikhil Garg, and Jacob Steinhardt; NeurIPS, 2023.	Formalized	0/36	65,464	Report Lean statements Dependency map Review packet Repo Formalization gap: Theorem 2 uses a specific two-dimensional user model; Theorems 3–4 cover user vectors at angles below 90°; Lemma 2 proves a restricted equilibrium characterization.
Axioms for AI Alignment from Human Feedback by Luise Ge, Daniel Halpern, Evi Micha, Ariel D. Procaccia, Itai Shapira, Yevgeniy Vorobeychik, and Junlin Wu; NeurIPS, 2024.	Formalized	0/27	9,919	Report Lean statements Dependency map Review packet Repo
Monoculture in Matching Markets by Kenny Peng, Nikhil Garg; NeurIPS, 2024.	Formalized	0/13	27,861	Report Lean statements Dependency map Review packet Repo
Quantifying Spatial Under-reporting Disparities in Resident Crowdsourcing by Zhi Liu, Uma Bhandaram, Nikhil Garg; Nature Computational Science, 2024.	Formalized	0/17	30,584	Report Lean statements Dependency map Review packet Repo
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.	Formalized	0/25	63,979	Report Lean statements Dependency map Review packet Repo
Redesigning Service Level Agreements: Equity and Efficiency in City Government Operations by Zhi Liu and Nikhil Garg; ACM EC, 2024.	Formalized	0/10	70,448	Report Lean statements Dependency map Review packet Repo
User-item fairness tradeoffs in recommendations by Sophie Greenwood, Sudalakshmee Chiniah, and Nikhil Garg; NeurIPS, 2024.	Formalized	0/23	51,656	Report Lean statements Dependency map Review packet Repo
Wisdom and Foolishness of Noisy Matching Markets by Kenny Peng, Nikhil Garg; ACM EC, 2024.	Formalized	0/25	73,910	Report Lean statements Dependency map Review packet Repo Formalization gap: Proposition 1 and Propositions 7(ii)-8 have their qualitative limits proved, while the source polynomial rates remain unproved.
A No Free Lunch Theorem for Human-AI Collaboration by Kenny Peng, Nikhil Garg, Jon Kleinberg; AAAI, 2025.	Formalized	0/5	8,372	Report Lean statements Dependency map Review packet Repo
Addressing Discretization-Induced Bias in Demographic Prediction by Evan Dong, Aaron Schein, Yixin Wang, and Nikhil Garg; PNAS Nexus, 2025.	Formalized	0/9	27,842	Report Lean statements Dependency map Review packet Repo
Balancing Producer Fairness and Efficiency via Prior-Weighted Rating System Design by Thomas Ma, Michael S. Bernstein, Ramesh Johari, and Nikhil Garg; ICWSM, 2025.	Formalized	0/2	633	Report Lean statements Dependency map Review packet Repo
Capacity Constraints Make Admissions Processes Less Predictable by Evan Dong; Nikhil Garg; Sarah Dean; AAAI-26 published version, DOI 10.1609/aaai.v40i45.41179.	Formalized	0/42	13,310	Report Lean statements Dependency map Review packet Repo
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.	Formalized	0/2	17,097	Report Lean statements Dependency map Review packet Repo
EFX for Additive Chores: Nonexistence, Pareto Incompatibility, and Bi-Valued Existence by Wentao He and Biaoshuai Tao; arXiv:2606.08872v2, 2026.	Formalized	0/18	40,537	Report Lean statements Dependency map Review packet Repo
Truth Revelation in Approximately Efficient Combinatorial Auctions by Daniel Lehmann, Liadan Ita O'Callaghan, and Yoav Shoham; Journal of the ACM, 2002.	Partially formalized	0/12	7,978	Report Lean statements Dependency map Review packet Repo Formalization gap: twelve selected auction-theoretic results are proved; Theorem 6.1's native NP-hardness and NP = ZPP consequences remain unproved.
On Approximately Fair Allocations of Indivisible Goods by Richard J. Lipton, Evangelos Markakis, Elchanan Mossel, and Amin Saberi; ACM EC, 2004.	Partially formalized	0/6	80,669	Report Lean statements Dependency map Review packet Repo Formalization gap: selected components of Theorems 2.1, 2.3, and 4.2 are proved; their remaining complexity and asymptotic clauses and Theorems 3.1-3.3 remain unproved.

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 5.5 or Codex 5.6 Terra, with xhigh thinking). Give the agent the paper link and exact source version, and ask it to follow the repository’s formalization and validation workflow. (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.