{"id":"palomar/PALOMAR-2026-10-01-000008","url":"https://github.com/Arthur742Ramos/roberts-theorem-lean/tree/0c176c66d2afa62301297f443b1e40eda2387ca2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000008-v1.json","repo":"https://github.com/Arthur742Ramos/roberts-theorem-lean","tags":["cs.GT","econ.TH","msc:91B14","mechanism-design","social-choice","affine-maximizers","lean"],"score":0,"title":"roberts-theorem-lean","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"cs.GT","summary":"A Lean formalization of Roberts theorem: for finite nonempty agent and alternative types with at least three alternatives, every onto dominant-strategy incentive compatible choice function is an affine maximizer. The proof follows the modular route: the taxation principle and weak monotonicity, reduction to strong monotonicity by tie-breaking, no-veto-power range analysis, the two-agent affine price representation, and induction on the number of agents.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"The characterization of implementable choice rules","identifier":"","relationship":"formalizes"},{"title":"A Modular Approach to Roberts Theorem","identifier":"","relationship":"formalizes"}]}