@article{Vickrey1961,
 author = {Vickrey, William},
 title = {Counterspeculation, Auctions, and Competitive Sealed Tenders},
 journal = {The Journal of Finance},
 volume = {16}, number = {1}, pages = {8--37}, year = {1961},
 doi = {10.1111/j.1540-6261.1961.tb02789.x},
 note = {\url{https://doi.org/10.1111/j.1540-6261.1961.tb02789.x}}
}
@article{Clarke1971,
 author = {Clarke, Edward H.},
 title = {Multipart Pricing of Public Goods},
 journal = {Public Choice},
 volume = {11}, pages = {17--33}, year = {1971},
 doi = {10.1007/BF01726210},
 note = {\url{https://doi.org/10.1007/BF01726210}}
}
@article{Groves1973,
 author = {Groves, Theodore},
 title = {Incentives in Teams},
 journal = {Econometrica},
 volume = {41}, number = {4}, pages = {617--631}, year = {1973},
 doi = {10.2307/1914085},
 note = {\url{https://doi.org/10.2307/1914085}}
}
@article{GreenLaffont1977,
 author = {Green, Jerry and Laffont, Jean-Jacques},
 title = {Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods},
 journal = {Econometrica},
 volume = {45}, number = {2}, pages = {427--438}, year = {1977},
 doi = {10.2307/1911219},
 note = {\url{https://doi.org/10.2307/1911219}}
}
@article{Holmstrom1979,
 author = {Holmstr{\"o}m, Bengt},
 title = {{Groves}' Scheme on Restricted Domains},
 journal = {Econometrica},
 volume = {47}, number = {5}, pages = {1137--1144}, year = {1979},
 doi = {10.2307/1911954},
 note = {\url{https://doi.org/10.2307/1911954}}
}
@inproceedings{Mathlib2020,
 author = {{The mathlib Community}},
 title = {The {Lean} mathematical library},
 booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 year = {2020}, pages = {367--381}, publisher = {ACM},
 doi = {10.1145/3372885.3373824},
 note = {\url{https://doi.org/10.1145/3372885.3373824}}
}
@misc{VCGArtifact,
 author = {Ramos, Arthur Freitas},
 title = {{Green--Laffont} characterization of {Groves} payments in {Lean}},
 year = {2026}, howpublished = {Version-pinned source repository},
 note = {Revision \nolinkurl{aad0c41b99053cf4657d91f7446279557f87ae18}, accessed September 30, 2026. \url{https://github.com/Arthur742Ramos/vcg-mechanism-lean/tree/aad0c41b99053cf4657d91f7446279557f87ae18}}
}
@misc{AFP2015,
 author = {Caminati, Marco B. and Kerber, Manfred and Lange, Christoph and Rowat, Colin},
 title = {{VCG} -- Combinatorial {Vickrey--Clarke--Groves} Auctions},
 howpublished = {Archive of Formal Proofs},
 year = {2015},
 note = {\url{https://isa-afp.org/entries/Vickrey_Clarke_Groves.html}}
}
@inproceedings{Barthe2016,
 author = {Barthe, Gilles and Gaboardi, Marco and Gallego Arias, Emilio Jes{\'u}s and Hsu, Justin and Roth, Aaron and Strub, Pierre-Yves},
 title = {Computer-Aided Verification for Mechanism Design},
 booktitle = {Web and Internet Economics},
 series = {Lecture Notes in Computer Science},
 volume = {10123}, pages = {279--293}, publisher = {Springer},
 year = {2016}, doi = {10.1007/978-3-662-54110-4_20},
 note = {\url{https://doi.org/10.1007/978-3-662-54110-4_20}. Full version, Appendix B: \url{https://arxiv.org/abs/1502.04052}}
}