HEXAGONbeta

A Lean Formalization of Roberts Theorem on Unrestricted Valuations

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 formalization of the finite unrestricted-domain version of Roberts theorem. For finite nonempty agent and alternative types, with at least three alternatives, an onto deterministic direct-revelation mechanism that is dominant-strategy incentive compatible has an affine-maximizer choice rule. Valuations range over all real-valued profiles; the conclusion uses fixed nonnegative weights, at least one nonzero, and alternative offsets, and asserts membership in the maximizing set. The development follows the modular proof route: taxation and weak monotonicity, perturbation-based tie-breaking to strong monotonicity, no-veto range analysis, affine prices for two agents, and induction through fixed-report slices. We explain the proved tie-set transport lemma, the construction of fresh payments for the tie-broken rule, and the transfer back to arbitrary ties. A version-pinned account distinguishes the proved library from statement-only comparator placeholders and separates source inspection from executable checks. This is an exposition of a classical result and its formal artifact, with no claim of mathematical novelty or formalization priority.

Provenance statement

Drafted primarily with GPT-6.1 assistance for exposition, source alignment, and typesetting. Some human understanding informed the work; no claim is made that every listed author independently understands every proof step. The Lean repository separately reports GPT-6-Luna assistance for formalization and packaging. Pinned public source: https://github.com/Arthur742Ramos/roberts-theorem-lean/tree/0c176c66d2afa62301297f443b1e40eda2387ca2, inspected September 30, 2026. Lean v4.35.0-rc2; Mathlib manifest revision 065356127b1dc0016f66b7283ce0ce2c4055aa55. The main theorem is DSIC plus onto implies nonnegative nontrivial affine-score argmax membership for finite nonempty agents and alternatives with at least three alternatives and unrestricted real valuations. The proved library has no sorry or custom axiom declarations; Challenge has three intentional comparator placeholders, outside the solution import chain. A successful September 27 Palomar mechanical run, 36327496620, concerns the earlier revision 61bd2b9075588716550bcd3ac9bc68f7392e823f. Current Lean source is textually identical after removing module/public/expose annotations and blank lines; that comparison is not a fresh Lean build of the new packaging. Model-assisted manuscript review is not independent human peer review. Manuscript and source are CC BY 4.0; referenced Lean repository is BSD-3-Clause.

Tools used

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

References

  1. Dobzinski, Shahar; Nisan, Noam. A Modular Approach to Roberts' Theorem. Algorithmic Game Theory, SAGT 2009, vol. 5814, pp. 14–23. 2009. \urlhttps://doi.org/10.1007/978-3-642-04645-2_3DOI
  2. Lavi, Ron; Mu'alem, Ahuva; Nisan, Noam. Towards a Characterization of Truthful Combinatorial Auctions. Proceedings of the 44th Annual IEEE Symposium on Foundations of Computer Science, pp. 574–583. 2003. \urlhttps://doi.org/10.1109/SFCS.2003.1238230DOI
  3. Palomar Registry. Mechanical verification of submission ujjeis5lup8v. 2026. Completed successfully September 27, 2026; submitted source revision 61bd2b9075588716550bcd3ac9bc68f7392e823f; not mathematical peer review
  4. Ramos, Arthur Freitas. Local verification record in the Roberts packaging commit. 2026. September 27, 2026; project-reported local checks, not external review
  5. Ramos, Arthur Freitas. roberts-theorem-lean: a Lean formalization of Roberts theorem. 2026. Pinned source inspected September 30, 2026; Lean and Mathlib v4.35.0-rc2
  6. Roberts, Kevin W. S. The characterization of implementable choice rules. Aggregation and Revelation of Preferences, pp. 321–349. 1979

Version history

  1. v1Initial depositCurrentSep 30, 2026