{"id":"hexagon/2609.00151","pdf":"https://hexagonmath.org/pdf/2609.00151v1","url":"https://hexagonmath.org/abs/2609.00151v1","tags":["cs.LO","msc:91B14","msc:68V20","Lean 4","Roberts theorem","affine maximizers","dominant strategies","formalization","mechanism design"],"score":0,"title":"A Lean Formalization of Roberts Theorem on Unrestricted Valuations","domain":"math.OC","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.OC","summary":"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,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["Codex","Codex"],"discussed":0,"published":"2026-09-30","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":false,"human_understanding":"some"}