{"id":"palomar/PALOMAR-2026-10-01-000012","url":"https://github.com/Arthur742Ramos/myerson-optimal-auction-lean/tree/f78aa142d4c34ed70262f44250fa66eb1f95ffb4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000012-v1.json","repo":"https://github.com/Arthur742Ramos/myerson-optimal-auction-lean","tags":["cs.GT","econ.TH","msc:91B26","auction-theory","mechanism-design","optimal-auctions","lean"],"score":0,"title":"Myerson's Optimal Auction Theorem","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"cs.GT","summary":"A Lean formalization of Myerson's 1981 optimal auction theorem, regular case, in a single-parameter independent-private-values model with real types. Finitely many bidders draw independent types from TypeDist priors: probability measures on ℝ with a continuous monotone CDF and a nonnegative Lebesgue density that vanishes for negative types, so each prior's mass lies on [0, ∞). The formal results are MyersonOptimalAuction.Palomar.virtualSurplusIdentity: under BIC, the support hypothesis (hsupp : ∀ t : ℝ, 0 0 so zero is in the support), and five integrability hypotheses, the expected payment…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"Optimal Auction Design","identifier":"","relationship":"formalizes"}]}