# 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 human-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).

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/7 | 7/7 covered | 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](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/29 | 29/29 covered | 8,931 |  |
| [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/30 | 30/30 covered | 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](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/43 | 43/43 covered | 13,741 |  |
| [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/26 | 24/24 covered | 133,338 |  |
| [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/55 | 27/28 covered; 1 support-only | 85,832 |  |
| [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/17 | 17/17 covered | 35,059 |  |
| [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/15 | 15/15 covered | 7,044 |  |
| [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 | 49/49 covered | 65,666 |  |
| [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/23 | 23/23 covered | 125,744 |  |
| [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/36 | 34/36 covered; 2 conditional boundaries | 142,959 |  |
| [Optimal Strategies in Ranked-Choice Voting](https://arxiv.org/abs/2407.13661) by Sanyukta Deshpande; Nikhil Garg; Sheldon H. Jacobson; arXiv:2407.13661, 2024; working paper. | [Formalized](../papers/DGJ24OptimalStrategiesRCV/FINAL_VALIDATION_REPORT.md) | 0/65 | 67/69 covered; 2 conditional boundaries | 54,427 |  |
| [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/42 | 40/42 covered; 2 conditional boundaries | 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](https://openreview.net/pdf?id=ZOZjMs3JTs) by Sophie Greenwood, Sudalakshmee Chiniah, and Nikhil Garg; NeurIPS, 2024. | [Formalized](../papers/GCG24UserItemFairness/FINAL_VALIDATION_REPORT.md) | 0/48 | 48/48 covered | 46,186 |  |
| [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/15 | 15/15 covered | 2,032 |  |
| [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/41 | 41/41 covered | 26,133 |  |
| [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) | 10/27 | 24/27 covered; 3 conditional boundaries | 680 | Strict variance decrease is formalized with the explicit interior-quality assumption 0 < q_v < 1. |
| [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/66 | 39/39 covered | 11,553 |  |
| [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/19 | 19/19 covered | 9,398 |  |
| [Simpler Than You Think: The Practical Dynamics of Ranked Choice Voting](https://arxiv.org/abs/2602.14329) by Sanyukta Deshpande; Nikhil Garg; Sheldon H. Jacobson; Journal of Computational Social Science, 2026. | [Formalized](../papers/DGJ26PracticalDynamicsRCV/FINAL_VALIDATION_REPORT.md) | 0/50 | 44/44 covered | 20,752 |  |
| [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/39 | 31/39 covered; 8 conditional boundaries | 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](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/44 | 37/49 covered; 12 conditional boundaries | 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](https://www.jair.org/index.php/jair/article/view/11358) by Nikhil Garg; Vijay Kamble; Ashish Goel; David Marn; Kamesh Munagala; JAIR 64, 2019. | [Partially formalized](../papers/GKGMM19IterativeLocalVoting/FINAL_VALIDATION_REPORT.md) | 0/47 | 39/48 covered; 8 conditional boundaries; 1 out of scope | 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](https://www.nature.com/articles/s43588-023-00572-6) by Zhi Liu, Uma Bhandaram, Nikhil Garg; Nature Computational Science, 2024. | [Partially formalized](../papers/LBG24SpatialUnderreporting/FINAL_VALIDATION_REPORT.md) | 0/25 | 16/24 covered; 8 conditional boundaries | 18,557 | Full formalization requires a homogeneous Poisson process and stopping-time derivation. |

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