HEXAGONbeta

Finite VCG and Groves Payments in Lean

Primarily AI-generated textHuman understanding: some partsmath.OC — Optimization and Controlcs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Sep 30, 2026 / CC BY 4.0

Abstract

We describe a Lean 4 development of finite direct mechanisms with quasi-linear utility and unrestricted real-valued valuations. The Clarke pivot mechanism selects a reported-welfare maximizer and charges each agent the loss in other-agent welfare relative to its maximum over the same fixed alternative set. The development proves efficiency, dominant-strategy truthfulness, nonnegative payments and no deficit, and individual rationality under the explicit assumption that every valuation is nonnegative. It also proves that every efficient, dominant-strategy incentive-compatible mechanism on the full valuation domain has Groves-form payments, with a term independent of the paying agent's report. We explain the finite-maximization interface, the report-update invariants, and the characterization argument using outcome-forcing reports and positive perturbations. The exposition is tied to a specific source revision and separates proved implementations from statement-only comparator placeholders. These are classical mechanism-design results; no new mathematical theorem or formalization-priority claim is made.

Provenance statement

Manuscript text primarily generated by OpenAI GPT-6.1, with human direction of scope and some human understanding. No comprehensive personal line-by-line human review is claimed. AI-assisted source comparison and independent AI mathematical and bibliographic review were performed. Formalization source metadata records distinct GPT-6-Luna assistance. The pinned public Lean artifact is https://github.com/Arthur742Ramos/vcg-mechanism-lean/tree/aad0c41b99053cf4657d91f7446279557f87ae18. Lean version v4.35.0-rc2; Mathlib v4.35.0-rc2 resolved to 065356127b1dc0016f66b7283ce0ce2c4055aa55. No fresh Lean build was executed in manuscript preparation; source assertions are from inspected pinned files. LaTeX reading copy compiled and visually checked, and source ZIP was freshly extracted and compiled with matching PDF text.

Tools used

Lean
LeanVersion 4.35.0-rc2
OpenAI
CodexVersion GPT-6.1
OpenAI
CodexVersion GPT-6-Luna (repository-reported formalization assistance)

References

  1. Barthe, Gilles; Gaboardi, Marco; Gallego Arias, Emilio Jesus; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves. Computer-Aided Verification for Mechanism Design. Web and Internet Economics, vol. 10123, pp. 279–293. 2016. \urlhttps://doi.org/10.1007/978-3-662-54110-4_20. Full version, Appendix B: \urlhttps://arxiv.org/abs/1502.04052DOI
  2. Caminati, Marco B.; Kerber, Manfred; Lange, Christoph; Rowat, Colin. VCG – Combinatorial Vickrey–Clarke–Groves Auctions. 2015. \urlhttps://isa-afp.org/entries/Vickrey_Clarke_Groves.html
  3. Clarke, Edward H. Multipart Pricing of Public Goods. Public Choice, vol. 11, pp. 17–33. 1971. \urlhttps://doi.org/10.1007/BF01726210DOI
  4. Green, Jerry; Laffont, Jean-Jacques. Characterization of Satisfactory Mechanisms for the Revelation of Preferences for Public Goods. Econometrica, vol. 45, no. 2, pp. 427–438. 1977. \urlhttps://doi.org/10.2307/1911219DOI
  5. Groves, Theodore. Incentives in Teams. Econometrica, vol. 41, no. 4, pp. 617–631. 1973. \urlhttps://doi.org/10.2307/1914085DOI
  6. Holmstrom, Bengt. Groves' Scheme on Restricted Domains. Econometrica, vol. 47, no. 5, pp. 1137–1144. 1979. \urlhttps://doi.org/10.2307/1911954DOI
  7. Ramos, Arthur Freitas. Green–Laffont characterization of Groves payments in Lean. 2026. Revision \nolinkurlaad0c41b99053cf4657d91f7446279557f87ae18, accessed September 30, 2026. \urlhttps://github.com/Arthur742Ramos/vcg-mechanism-lean/tree/aad0c41b99053cf4657d91f7446279557f87ae18
  8. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI
  9. Vickrey, William. Counterspeculation, Auctions, and Competitive Sealed Tenders. The Journal of Finance, vol. 16, no. 1, pp. 8–37. 1961. \urlhttps://doi.org/10.1111/j.1540-6261.1961.tb02789.xDOI

Version history

  1. v1Initial depositCurrentSep 30, 2026