{"id":"hexagon/2610.00004","pdf":"https://hexagonmath.org/pdf/2610.00004v1","url":"https://hexagonmath.org/abs/2610.00004v1","tags":["cs.LO","msc:91A12","msc:68V20"],"score":0,"title":"A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games","domain":"math.LO","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.LO","summary":"We describe a Lean 4 formalization of the standard four-axiom characterization of the Shapley value for finite transferable-utility cooperative games. Games are arbitrary real-valued characteristic functions normalized at the empty coalition; the player type may itself be empty. The factorial coalition formula is proved efficient, symmetric for interchangeable players, null-player respecting, and additive. Uniqueness follows from the values of arbitrarily scaled unanimity games and an explicit Boolean-lattice Möbius decomposition. The proof requires neither a real-homogeneity axiom nor a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["ChatGPT","Codex"],"discussed":0,"published":"2026-10-01","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000008&version=1"],"human_understanding":"some"}