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,675
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.	197,122
Foundations: optimization	Convex optimization and duality; gradient, subgradient, and mirror descent; stochastic optimization; proximal maps and projections; argmax stability and envelope theorems.	20,569
AI and applications	Alignment axioms and welfare; differential privacy and composition; algorithmic fairness; admissions policies; rating systems; recommender systems and producer/user fairness.	26,487
Learning and statistics	Generalization and sample complexity; calibration, multiaccuracy, and omniprediction; online learning and regret; bandits; reinforcement learning; preference learning and human feedback.	61,555
Algorithms and complexity	Online allocation and advertising; competitive analysis and regret reductions; primal-dual approximation arguments; computational complexity, reductions, and neural-network verification.	6,928
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	25,382	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. The continuous-outcome extension assumes a common monotone coupling and integrable revenue; deriving such a coupling from arbitrary marginal offer laws remains outside the checked result 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	28,430	Report Lean statements Dependency map Review packet Repo
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,988	Report Lean statements Dependency map Review packet Repo
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	55,549	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
Fair Allocation through Selective Information Acquisition by William Cai, Johann Gaebler, Nikhil Garg, Sharad Goel; AAAI/ACM AIES, 2020.	Formalized	0/5	12,387	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	13,293	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
Strategic ranking by Lydia T. Liu, Nikhil Garg, Christian Borgs; AISTATS / PMLR 151, 2022.	Formalized	0/18	51,185	Report Lean statements Dependency map Review packet Repo Proposition 3.1’s cutoff monotonicity and Proposition B.2’s optimum use the additional regularity conditions stated in the report.
Supply-Side Equilibria in Recommender Systems by Meena Jagadeesan, Nikhil Garg, and Jacob Steinhardt; NeurIPS, 2023.	Formalized	0/36	69,062	Report Lean statements Dependency map Review packet Repo Selected theoretical surface formalized: Theorem 2 covers arbitrary finite-dimensional two-user geometry; Theorems 3–4 prove the corrected strictly acute canonical two-genre construction; Lemma 2 uses the tie-aware corrected characterization. See FINAL_VALIDATION_REPORT.md.
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	12,227	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/19	30,658	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	64,182	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/19	75,243	Report Lean statements Dependency map Review packet Repo Appendix polynomial-rate results use the documented lower-tail correction and finite-second-moment condition.
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
Distortion of AI Alignment: Does Preference Optimization Optimize for Preferences? by Paul Gölz, Nika Haghtalab, and Kunhe Yang; NeurIPS, 2025.	Formalized	0/16	23,210	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	3/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	12,186	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.
How Many Features Can a Language Model Store Under the Linear Representation Hypothesis? by Nikhil Garg, Jon Kleinberg, Kenny Peng; arXiv:2602.11246v1, 2026.	Partially formalized	0/11	11,528	Report Lean statements Dependency map Review packet Repo Theorem 3, Corollary 8, Theorem 12, and Corollary 13 use the cited Alon rank theorem as an external assumption.
A Testable Theory of Atomic Features by Kenny Peng, Jon Kleinberg, and Nikhil Garg; Working paper, 2026.	Formalized	—	39,335	Report Lean statements Theorem index Repo Reference folder Maintained in a separate repository.

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.