# Paper Status

This file is generated by `python3 scripts/sync_paper_status.py` from
paper-local `papers/<PaperName>/status.json` files. Edit those sources
rather than this table.

The table is intentionally public-facing. `Note` is blank for
formalized papers unless a source-version, proof-route, or remaining-boundary
note is useful to a public reader. For detailed machine-readable metadata,
see [`papers/status.json`](../papers/status.json); for the compact public
JSON, see [`papers/human_status.json`](../papers/human_status.json).
Paper-local records marked `repository_visibility: private_only` remain
in the aggregate private index but are excluded from this public table.

Human-review counts are dashboard rows saved by a human reviewer; agent
source audits are not counted as human review.

Paper IDs and folder names are stable artifact identifiers and may track
an arXiv, conference, or original working-paper year. The table below uses
the published citation title and year.

| Paper, authors, publication | Status | Human review | Paper coverage | Lines of Code | Public note |
|---|---|---:|---:|---:|---|
| [College Admissions and the Stability of Marriage](https://www.jstor.org/stable/2312726) by D. Gale and L. S. Shapley; American Mathematical Monthly, 1962. | [Formalized](../papers/GS62CollegeAdmissions/FINAL_VALIDATION_REPORT.md) | 0/6 | accepted closeout: 6/6 source claims covered | 5,467 |  |
| [The Regulation of Queue Size by Levying Tolls](https://www.jstor.org/stable/1909200) by P. Naor; Econometrica 37(1), 1969. | [Formalized](../papers/Naor1969QueueTolls/FINAL_VALIDATION_REPORT.md) | 0/6 | accepted closeout: 6/6 source claims covered | 922 | Few lines of code as much of machinery is in the shared library |
| [The Economics of Matching: Stability and Incentives](https://pubsonline.informs.org/doi/epdf/10.1287/moor.7.4.617) by Alvin E. Roth; Mathematics of Operations Research, 1982. | [Formalized](../papers/Roth82StableMatching/FINAL_VALIDATION_REPORT.md) | 0/10 | accepted closeout: 10/10 source claims covered | 11,294 |  |
| [Optimal Incentive-Compatible Priority Pricing for the M/M/1 Queue](https://pubsonline.informs.org/doi/10.1287/opre.38.5.870) by Haim Mendelson and Seungjin Whang; Operations Research 38(5), 1990. | [Formalized](../papers/MendelsonWhang1990PriorityPricing/FINAL_VALIDATION_REPORT.md) | 0/5 | accepted closeout: 5/5 source claims covered | 3,616 | 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](https://doi.org/10.1006/jcss.1997.1504) by Yoav Freund and Robert E. Schapire; Journal of Computer and System Sciences 55(1):119–139, 1997. | [Formalized](../papers/FreundSchapire1997Hedge/FINAL_VALIDATION_REPORT.md) | 0/14 | accepted closeout: 14/14 source claims covered | 1,136 | Few lines of code as much of machinery is in the shared library |
| [Competitive Auctions and Digital Goods](https://www.cs.miami.edu/home/burt/learning/Csc597.052/docs/goldberg.pdf) by Andrew V. Goldberg, Jason D. Hartline, and Andrew Wright; SODA, 2001. | [Formalized](../papers/GHW01DigitalGoods/FINAL_VALIDATION_REPORT.md) | 0/12 | accepted closeout: 12/12 source claims covered | 24,842 | 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](https://www.sciencedirect.com/science/article/pii/S0899825606000303). |
| [AdWords and Generalized Online Matching](https://people.eecs.berkeley.edu/~vazirani/pubs/adwords.pdf) by Aranyak Mehta, Amin Saberi, Umesh Vazirani, and Vijay V. Vazirani; Journal of the ACM, 2007. | [Formalized](../papers/MSVV07AdWords/FINAL_VALIDATION_REPORT.md) | 0/50 | accepted closeout: 50/50 source claims covered | 22,118 | 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](https://www.nber.org/papers/w11765) by Benjamin Edelman, Michael Ostrovsky, and Michael Schwarz; American Economic Review, 2007. | [Formalized](../papers/EOS07GSP/FINAL_VALIDATION_REPORT.md) | 0/13 | accepted closeout: 13/13 source claims covered | 142,501 | 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](https://proceedings.neurips.cc/paper/2017/hash/db98dc0dbafde48e8f74c0de001d35e4-Abstract.html) by Moein Falahatgar, Yi Hao, Alon Orlitsky, Venkatadheeraj Pichapati, and Vaishakh Ravindrakumar; NeurIPS, 2017. | [Formalized](../papers/FalahatgarEtAl2017MaxingRanking/FINAL_VALIDATION_REPORT.md) | 0/23 | accepted closeout: 23/23 source claims covered | 33,818 |  |
| [Designing Optimal Binary Rating Systems](https://proceedings.mlr.press/v89/garg19a/garg19a.pdf) by Nikhil Garg, Ramesh Johari; AISTATS / PMLR 89, 2019. | [Formalized](../papers/GJ19OptimalBinaryRatingSystems/FINAL_VALIDATION_REPORT.md) | 0/33 | accepted closeout: 33/33 source claims covered | 96,123 | 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](https://arxiv.org/abs/2001.07042v1) by Arjun Seshadri and Johan Ugander; ACM EC 2019; arXiv version (2020). | [Formalized](../papers/SeshadriUgander2020IIATesting/FINAL_VALIDATION_REPORT.md) | 0/11 | accepted closeout: 11/11 source claims covered | 10,986 |  |
| [Iterative Local Voting for Collective Decision-making in Continuous Spaces](https://www.jair.org/index.php/jair/article/view/11358) by Nikhil Garg; Vijay Kamble; Ashish Goel; David Marn; Kamesh Munagala; JAIR 64, 2019. | [Formalized](../papers/GKGMM19IterativeLocalVoting/FINAL_VALIDATION_REPORT.md) | 0/12 | accepted closeout: 12/12 source claims covered | 54,809 | 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](https://arxiv.org/pdf/1906.08160) by Nikhil Garg; Lodewijk Gelauff; Sukolsak Sakshuwong; Ashish Goel; HCOMP, 2019. | [Formalized](../papers/GGSG19TopThree/FINAL_VALIDATION_REPORT.md) | 0/15 | accepted closeout: 15/15 source claims covered | 38,678 |  |
| [Axioms for Learning from Pairwise Comparisons](https://proceedings.neurips.cc/paper_files/paper/2020/hash/cdaa9b682e10c291d3bbadca4c96f5de-Abstract.html) by Ritesh Noothigattu, Dominik Peters, and Ariel D. Procaccia; NeurIPS, 2020. | [Formalized](../papers/NoothigattuEtAl2020PairwiseComparisons/FINAL_VALIDATION_REPORT.md) | 0/10 | accepted closeout: 10/10 source claims covered | 2,507 |  |
| [Designing Informative Rating Systems: Evidence from an Online Labor Market](https://doi.org/10.1287/msom.2020.0921) by Nikhil Garg, Ramesh Johari; Manufacturing & Service Operations Management 23(3), 2020. | [Formalized](../papers/GJ18InformativeRatingSystems/FINAL_VALIDATION_REPORT.md) | 0/3 | accepted closeout: 3/3 source claims covered | 9,718 |  |
| [Performative Prediction](https://proceedings.mlr.press/v119/perdomo20a.html) by Juan C. Perdomo, Tijana Zrnic, Celestine Mendler-Dünner, and Moritz Hardt; ICML, 2020. | [Formalized](../papers/PZMH20PerformativePrediction/FINAL_VALIDATION_REPORT.md) | 0/11 | accepted closeout: 11/11 source claims covered | 3,813 | 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](https://www.pnas.org/doi/10.1073/pnas.2018340118) by Jon Kleinberg and Manish Raghavan; PNAS, 2021. | [Formalized](../papers/KR21Monoculture/FINAL_VALIDATION_REPORT.md) | 0/49 | accepted closeout: 49/49 source claims covered | 116,134 |  |
| [Test-optional Policies: Overcoming Strategic Behavior and Informational Gaps](https://arxiv.org/pdf/2107.08922) by Zhi Liu and Nikhil Garg; EAAMO, 2021. | [Formalized](../papers/LG21TestOptionalPolicies/FINAL_VALIDATION_REPORT.md) | 0/15 | accepted closeout: 15/15 source claims covered | 210,358 | 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](https://arxiv.org/abs/2201.10408v4) by Ira Globus-Harris, Michael Kearns, and Aaron Roth; ACM FAccT, 2022. | [Formalized](../papers/GHKR22BiasBounties/FINAL_VALIDATION_REPORT.md) | 0/15 | accepted closeout: 15/15 source claims covered | 14,755 |  |
| [Driver Surge Pricing](https://arxiv.org/pdf/1905.07544) by Nikhil Garg and Hamid Nazerzadeh; Management Science, 2022. | [Formalized](../papers/GN21DriverSurgePricing/FINAL_VALIDATION_REPORT.md) | 0/16 | accepted closeout: 16/16 source claims covered | 203,502 |  |
| [Supply-Side Equilibria in Recommender Systems](https://arxiv.org/abs/2206.13489v3) by Meena Jagadeesan, Nikhil Garg, and Jacob Steinhardt; NeurIPS, 2023. | [Formalized](../papers/JGS23SupplySideRecommenderSystems/FINAL_VALIDATION_REPORT.md) | 0/36 | accepted closeout: 36/36 source claims covered | 65,464 | 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](https://proceedings.neurips.cc/paper_files/paper/2024/hash/9328208f88ec69420031647e6ff97727-Abstract-Conference.html) by Luise Ge, Daniel Halpern, Evi Micha, Ariel D. Procaccia, Itai Shapira, Yevgeniy Vorobeychik, and Junlin Wu; NeurIPS, 2024. | [Formalized](../papers/GeEtAl2024AlignmentAxioms/FINAL_VALIDATION_REPORT.md) | 0/27 | accepted closeout: 27/27 source claims covered | 9,919 |  |
| [Monoculture in Matching Markets](https://papers.nips.cc/paper_files/paper/2024/hash/95249d42f559a0cfaf282fdf26fe2e69-Abstract-Conference.html) by Kenny Peng, Nikhil Garg; NeurIPS, 2024. | [Formalized](../papers/PG23MonocultureMatching/FINAL_VALIDATION_REPORT.md) | 0/13 | accepted closeout: 13/13 source claims covered | 27,861 |  |
| [Quantifying Spatial Under-reporting Disparities in Resident Crowdsourcing](https://www.nature.com/articles/s43588-023-00572-6) by Zhi Liu, Uma Bhandaram, Nikhil Garg; Nature Computational Science, 2024. | [Formalized](../papers/LBG24SpatialUnderreporting/FINAL_VALIDATION_REPORT.md) | 0/17 | accepted closeout: 17/17 source claims covered | 30,584 |  |
| [Reconciling the Accuracy-Diversity Trade-off in Recommendations](https://arxiv.org/abs/2307.15142) by Kenny Peng, Manish Raghavan, Emma Pierson, Jon Kleinberg, and Nikhil Garg; The ACM Web Conference, 2024. | [Formalized](../papers/PRPKG24AccuracyDiversity/FINAL_VALIDATION_REPORT.md) | 0/25 | accepted closeout: 25/25 source claims covered | 63,979 |  |
| [Redesigning Service Level Agreements: Equity and Efficiency in City Government Operations](https://arxiv.org/abs/2410.14825) by Zhi Liu and Nikhil Garg; ACM EC, 2024. | [Formalized](../papers/LG24ServiceLevelAgreements/FINAL_VALIDATION_REPORT.md) | 0/10 | accepted closeout: 10/10 source claims covered | 70,448 |  |
| [User-item fairness tradeoffs in recommendations](https://openreview.net/pdf?id=ZOZjMs3JTs) by Sophie Greenwood, Sudalakshmee Chiniah, and Nikhil Garg; NeurIPS, 2024. | [Formalized](../papers/GCG24UserItemFairness/FINAL_VALIDATION_REPORT.md) | 0/23 | accepted closeout: 23/23 source claims covered | 51,656 |  |
| [Wisdom and Foolishness of Noisy Matching Markets](https://arxiv.org/abs/2402.16771) by Kenny Peng, Nikhil Garg; ACM EC, 2024. | [Formalized](../papers/PG24NoisyMatchingMarkets/FINAL_VALIDATION_REPORT.md) | 0/25 | accepted closeout: 25/25 source claims covered | 73,910 | 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](https://ojs.aaai.org/index.php/AAAI/article/view/33574) by Kenny Peng, Nikhil Garg, Jon Kleinberg; AAAI, 2025. | [Formalized](../papers/PKG25NoFreeLunch/FINAL_VALIDATION_REPORT.md) | 0/5 | accepted closeout: 5/5 source claims covered | 8,372 |  |
| [Addressing Discretization-Induced Bias in Demographic Prediction](https://arxiv.org/pdf/2405.16762) by Evan Dong, Aaron Schein, Yixin Wang, and Nikhil Garg; PNAS Nexus, 2025. | [Formalized](../papers/DSWG24DiscretizationBias/FINAL_VALIDATION_REPORT.md) | 0/9 | accepted closeout: 9/9 source claims covered | 27,842 |  |
| [Balancing Producer Fairness and Efficiency via Prior-Weighted Rating System Design](https://arxiv.org/pdf/2207.04369) by Thomas Ma, Michael S. Bernstein, Ramesh Johari, and Nikhil Garg; ICWSM, 2025. | [Formalized](../papers/MBJG25ProducerFairness/FINAL_VALIDATION_REPORT.md) | 0/2 | accepted closeout: 2/2 source claims covered | 633 |  |
| [Capacity Constraints Make Admissions Processes Less Predictable](https://arxiv.org/abs/2601.11513) by Evan Dong; Nikhil Garg; Sarah Dean; AAAI-26 published version, DOI 10.1609/aaai.v40i45.41179. | [Formalized](../papers/DGD26AdmissionsPredictability/FINAL_VALIDATION_REPORT.md) | 0/42 | accepted closeout: 42/42 source claims covered | 13,310 |  |
| [Combatting Gerrymandering with Ranked Choice Voting: an Experimental Analysis of Multi-member Districts in the United States](https://doi.org/10.1287/opre.2024.1167) by Nikhil Garg; Wes Gurnee; David Rothschild; David Shmoys; Operations Research, 2026, DOI 10.1287/opre.2024.1167. | [Formalized](../papers/GGRS26CombattingGerrymanderingRCV/FINAL_VALIDATION_REPORT.md) | 0/2 | accepted closeout: 2/2 source claims covered | 17,097 |  |
| [EFX for Additive Chores: Nonexistence, Pareto Incompatibility, and Bi-Valued Existence](https://arxiv.org/abs/2606.08872v2) by Wentao He and Biaoshuai Tao; arXiv:2606.08872v2, 2026. | [Formalized](../papers/HT26EFXChores/FINAL_VALIDATION_REPORT.md) | 0/18 | accepted closeout: 18/18 source claims covered | 40,537 |  |
| [Truth Revelation in Approximately Efficient Combinatorial Auctions](https://jmvidal.cse.sc.edu/library/lehmann02a.pdf) by Daniel Lehmann, Liadan Ita O'Callaghan, and Yoav Shoham; Journal of the ACM, 2002. | [Partially formalized](../papers/LOS02CombinatorialAuctions/FINAL_VALIDATION_REPORT.md) | 0/12 | accepted closeout: 12/12 source claims covered | 7,978 | 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](https://www.cs.cmu.edu/~arielpro/15896s15/docs/paper12a.pdf) by Richard J. Lipton, Evangelos Markakis, Elchanan Mossel, and Amin Saberi; ACM EC, 2004. | [Partially formalized](../papers/LMMS04FairDivision/FINAL_VALIDATION_REPORT.md) | 0/6 | accepted closeout: 6/6 source claims covered | 80,669 | 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. |

For status vocabulary, see [`docs/STATUS.md`](STATUS.md).