math.LO — Logic
A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games
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 continuity assumption on competing allocation rules. We explain the finite-sum arguments, the precise Lean statements, the separation between the registry’s challenge and implemented solution, and the historical verification evidence for the pinned source revision. The contribution is an auditable exposition of an existing formalization of classical mathematics, with no claim of new mathematics or formalization priority.