A Lean Formalization of the Shapley Value Characterization for Finite Cooperative Games

Context and contribution

The Shapley value assigns a payoff to each player of a cooperative game by weighting that player’s marginal contributions to coalitions. Shapley’s classical work introduced a value characterized axiomatically [7]; subsequent developments and applications are collected in Roth’s edited volume [6]. This paper concerns the standard modern formulation using efficiency, symmetry, the null-player property, and additivity. It does not present that quartet as a literal transcription of the original paper’s axiom list.

The subject here is the Lean 4 and Mathlib development [1, 8, 4] registered as PALOMAR-2026-09-25-000008, version 1 [3]. Every source claim refers to commit ee15891fecdf294363791c61a5ec018109fe423a. The registered source credits Arthur Freitas Ramos as its author and responsible maintainer. The three-author byline above is the byline of this explanatory manuscript; it does not change the registered source attribution.

The development has two mathematically substantive parts. First, direct finite-sum manipulations show that the factorial formula satisfies all four axioms. In particular, efficiency is established by cancellation of coalition coefficients, rather than by a formal permutation-average representation. Second, unanimity games and a Boolean-lattice inversion formula show that any rule satisfying the axioms has a prescribed value on every game. The uniqueness proof is careful about the difference between additivity and real linearity: it determines arbitrary real multiples of unanimity games directly from the other three axioms.

Our contribution is to make the formal artifact’s exact scope, proof architecture, and evidence boundary accessible without requiring the reader to infer them from Lean syntax. The mathematical characterization and inversion method are classical. Neither registration

Copyright 2026 the authors. Licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). nor the present exposition establishes a priority claim, independent human review of every proof term, or an endorsement by the authors of the mathematical sources.

Games and the exact axioms

Let $N$ be a finite player type with decidable equality, and write $n = \lvert N\rvert$. Lean expresses these assumptions as [FintypeN] and [DecidableEqN]. Coalitions are finite sets of players, represented by FinsetN. The grand coalition is Finset.univ.

Definition 2.1. A game is a function $v:\mathcal{P}(N)\to\mathbb{R}$ satisfying $v(\varnothing)=0$. Write $\mathcal{G}(N)$ for the set of these games. Addition and real scalar multiplication are pointwise.

The source definition ShapleyValue.Game bundles the function with its normalization proof as a subtype. It does not impose positivity, monotonicity, superadditivity, convexity, or an assumption that $N$ is nonempty. Although the game type itself can be defined without a finite player assumption, the Shapley formula and the characterization use finite players throughout.

An allocation rule is an arbitrary function $\psi:\mathcal{G}(N)\to(N\to\mathbb{R})$. It need not initially be continuous, measurable, computable, or linear. Its four properties are as follows.

Definition 2.2. The rule $\psi$ is:

1. efficient if $\sum_{i\in N}\psi_i(v)=v(N)$ for every game $v$;

2. symmetric if, for every $v$ and $i,j\in N$,

   $$\left[\forall S\subseteq N,\ i,j\notin S\Rightarrow v(S\cup\{i\})=v(S\cup\{j\})\right]\Rightarrow\psi_i(v)=\psi_j(v);$$

3. null-player respecting if, for every $v$ and $i$,

   $$\left[\forall S\subseteq N,\ i\notin S\Rightarrow v(S\cup\{i\})=v(S)\right]\Rightarrow\psi_i(v)=0;$$

4. additive if $\psi_i(v+w)=\psi_i(v)+\psi_i(w)$ for all $v,w,i$.

These are exactly the predicates Efficient, Symmetric, NullPlayer, and Additive in the ShapleyValue namespace. Symmetry is a within-game condition on interchangeable players; the interface does not posit a separate cross-game relabeling axiom. The null-player property is the zero-marginal condition stated above, not a separately assumed general dummy-player payment formula.

For $1\le k\le n$, define

The Shapley formula implemented in shapleyValue is

Factorials are natural numbers cast to $\mathbb{R}$. The implementation defines weight for every natural $k$ using truncated natural subtraction, but only $1\le k\le n$ occurs in (2). The denominator $n!$ is nonzero even when $n=0$. In the coefficient identities below, $w_n$ denotes this total extension, including $k=0$ and $k=n+1$.

Theorem 2.3 (Registered characterization). For every finite player type $N$ and allocation rule $\psi$,

The public declaration is ShapleyValue.Palomar.shapley_characterization. Equality is equality of functions on every game and every player, not agreement only on a restricted class of games. If $N=\varnothing$, every payoff vector is the unique empty function, efficiency is $0=v(\varnothing)$, and the remaining player-indexed conditions are vacuous. The source retains this case instead of imposing a nonempty-player hypothesis.

The factorial formula satisfies the axioms

Null players and additivity

If $i$ is null and $i \in S$, apply the null hypothesis to $S \setminus\{i\}$ to obtain $v(S)=v(S \setminus\{i\})$. Every summand in (2) is therefore zero. For additivity, pointwise game addition gives

Distributivity and finite-sum additivity finish the argument. These are shapleyValue_nullPlayer and shapleyValue_additive in ShapleyValue/Existence.lean.

Symmetry by coalition reindexing

The insertion–erasure bijection rewrites the formula as

Suppose $i \ne j$ are interchangeable. Split each sum according to whether the other player belongs to $R$. Coalitions excluding both players give equal contributions by the symmetry hypothesis. In the other parts, write the coalitions as $R \cup\{j\}$ and $R \cup\{i\}$, respectively, where $R$ excludes both. The common upper coalition is $R \cup\{i,j\}$, the lower worths are equal, and the weights agree because the cardinalities agree. Thus $\phi_i(v)=\phi_j(v)$. The case $i=j$ is immediate.

The Lean proof shapleyValue_symmetric follows precisely this split. Its helper lemmas establish the insertion–erasure bijections as finite-sum reindexings, including their membership and inverse conditions.

Efficiency by weight cancellation

For $1 \le k<n$, the factorial identities give

When $n>0$, they also give $n\,w_n(n)=1$. These are the source lemmas weight_balance and weight_top.

Sum (2) over players and interchange the finite sums. Each $v(S)$ occurs $|S|$ times as an upper-coalition worth. For lower-coalition occurrences, set $T=S \setminus\{i\}$, so that $i \notin T$ and $S=T \cup\{i\}$. There are $n-|T|$ choices of such $i$. Consequently,

Every nonempty proper-coalition coefficient vanishes by (4). The empty-coalition term vanishes by normalization, regardless of the value of its coefficient. If $n>0$, the grand-coalition coefficient equals one, giving $v(N)$. If $n=0$, the only coalition is empty and both sides are zero.

The implementation shapleyValue_efficient makes all these boundary cases explicit. It uses sum_over_members, sum_over_nonmembers, and sum_filter_insert to obtain (5), rather than asserting an unproved interchange or a counting identity. This proves existence of an allocation rule satisfying the four axioms before uniqueness is invoked.

Unanimity games and uniqueness

Scaled unanimity games without a homogeneity axiom

For nonempty $T \subseteq N$, the unanimity game $u_T$ is

The Lean definition unanimityGame is total on all coalitions: $u_{\varnothing}$ is defined to be the zero game, so that normalization is never violated.

Lemma 4.1. If $\psi$ is efficient, symmetric, and null-player respecting, then for every nonempty $T$, every real $c$, and every player $i$,

Proof. Every player outside $T$ is null in $cu_T$, hence receives zero. Members of $T$ are interchangeable: for two distinct members and a coalition excluding both, inserting only one cannot complete $T$. Their payoffs are therefore equal. Efficiency and $(cu_T)(N)=c$ give $|T|$ times the common payoff equal to $c$. Since $T$ is nonempty, division by $|T|$ is valid. The argument also covers $c=0$ and $c<0$. $\square$

This is valueOn_unanimity. Notably, its assumptions do not include additivity. It does not infer $\psi(cu_T)=c\psi(u_T)$ from additivity: such an inference for arbitrary real $c$ would require justification. Instead, (6) is established directly for each scaled game. The later uniqueness proof needs only additivity over a finite sum.

Boolean-lattice inversion

Define the coefficient

implemented as mobiusCoeff. This is the Boolean-lattice Möbius transform; incidence-algebra inversion is treated generally by [5].

Lemma 4.2. For every normalized game $v$ and coalition $Q$,

Consequently, as games,

Proof. Expand the right side of (8) using (7) and interchange the two finite sums. For a nonempty $S\subseteq Q$, its worth $v(S)$ has coefficient

using the bijection $T\mapsto T\setminus S$, with inverse $U\mapsto S\cup U$. This alternating sum is one if $S=Q$ and zero otherwise. In the latter case $Q\setminus S$ is nonempty, and the sum vanishes by the binomial identity $(1-1)^{|Q\setminus S|}=0$. The $S=\varnothing$ term vanishes because $v(\varnothing)=0$. If $Q$ is empty, the sum in (8) is empty and the identity again follows from normalization. Evaluating the right side of (9) at $Q$ selects exactly its nonempty subsets, so (8) proves equality of games. $\square$

The source isolates the alternating cancellation in alt_sum_powerset and inner_mobius. The latter assumes a nonempty $S$, $S\subseteq Q$, and $S\ne Q$; empty $S$ is handled separately by normalization. The resulting pointwise and game-level theorems are mobius_pointwise and mobius_decomposition. Thus no coefficient is silently divided by a zero coalition size.

Determination of every allocation

Additivity first implies $\psi_i(0)=0$, since $\psi_i(0)=\psi_i(0)+\psi_i(0)$. Induction then extends it to any finite sum; this is additive_sum. Apply it to (9) and use Lemma 4.1 for each summand to obtain

The theorem value_eq_of_axioms proves this formula for every rule satisfying the four properties.

The rule $\phi$ satisfies those properties by Section 3, so it has the same expression (10). Any other such $\psi$ therefore agrees with $\phi$ at every game and player. Function extensionality gives shapleyValue_unique. Its converse, substituting $\psi= \phi$ and collecting the four existence results, proves Theorem 2.3. This proof uses no continuity axiom and does not assume a real-linear structure on the competing rule.

Remark 4.3 (An illustrative three-player calculation). Let $N = \{a,b,c\}$ and write $v_{ab} = v(\{a,b\})$, and similarly for other coalitions. For player $a$, formula (2) reads

Meanwhile (7) gives $m_v(\{a\}) = v_a$, $m_v(\{a,b\}) = v_{ab}-v_a-v_b$, and $m_v(N) = v_{abc}-v_{ab}-v_{ac}-v_{bc}+v_a+v_b+v_c$. Substitution into (10) gives the same expression. This calculation illustrates the two representations; it is explanatory algebra, not an additional registered theorem or source benchmark.

The formal interface and its evidence boundary

Implementation and challenge

The substantive source modules have distinct roles:

• ShapleyValue/Basic.lean: games, operations, factorial weight, the Shapley formula, and the four predicates;

• ShapleyValue/Existence.lean: finite-sum reindexing, weight cancellation, and the four properties of the formula;

• ShapleyValue/Uniqueness.lean: the additive game structure, unanimity games, inversion, determination of values, and characterization;

• Solution.lean: the six public wrapper theorems in the ShapleyValue.Palomar namespace.

Besides the characterization and uniqueness theorems, the exported wrappers are shapleyValue_efficient, shapleyValue_symmetric, shapleyValue_nullPlayer, and shapleyValue_additive, all under that namespace.

Challenge.lean is a separate specification module. It repeats the seven compared definitions and six theorem statements, each theorem ending in an intentional sorry. The solution imports the substantive uniqueness module, not the challenge. Compiling the challenge alone cannot establish the six results, and its six statement holes must not be mistaken for holes in the solution proof dependency chain. The comparator configuration fixes the compared definitions and theorems and permits only propext, Quot.sound, and Classical.choice as axioms.

Pinned environment and historical verification

The authoritative lean-toolchain selects leanprover/lean4:v4.35.0-rc2, and lake-manifest.json pins Mathlib to 065356127b1dc0016f66b7283ce0ce2c4055aa55, together with eight transitive packages. Reproduction should preserve the complete manifest. The README’s older reference to Lean 4.33.0 is inconsistent with this pin and is not the environment used for the registered verification. The separate local comparator script also has older-toolchain comments and pins; its compatibility should be checked before using it for a new replay.

The registry records successful verification on September 24, 2026, followed by registration on September 25. The official mechanical report from workflow run 36005001365 was retrieved during manuscript preparation [2]. It identifies the exact source commit, challenge and solution hashes, toolchain, dependencies, and permitted axioms. It reports a successful solution build and acceptance by Lean’s default kernel and by the con-ron and NanoDa kernels. Its status is pass, with no listed errors or warnings. The comparator’s kernel-acceptance statement concerns the solution checked against that configured challenge surface; it is historical machine-checking evidence, not a fresh run performed for this manuscript.

The three permitted foundations are propositional extensionality, quotient soundness, and classical choice. These are standard classical Lean foundations, not the four economic axioms, which are explicit hypotheses on $\psi$. A permitted-axiom list bounds what may occur in the checked proof dependency closure; by itself it does not say that each theorem uses all three. The pinned scripts/AxiomAudit.lean prints axiom dependencies for twelve declarations, consisting of the six library theorems and their six wrappers. Its checker requires exact coverage and rejects axioms outside the configured set. We inspected this audit’s source, but do not claim a new per-declaration axiom execution.

Checks performed for this exposition

Fresh source retrieval on October 1, 2026 checked all 22 repository blobs against the Git tree at the registered commit. The implementation modules and solution contain no visible sorry, admit, or new axiom declaration in this static inspection. The challenge contains exactly the six deliberate statement holes described above. Challenge, solution, manifest, and configuration hashes agree with the official mechanical report. A separate AI-based review checked the mathematical exposition against the pinned declarations and proof organization, and the bibliography against primary-source publication records.

No fresh Lean build, kernel replay, or executed axiom audit was performed while preparing this manuscript. Static scans cannot replace elaboration and transitive proof-term checking. The proofs in Sections 3 and 4 are mathematical explanations of the source architecture, not an alternative verification system. Likewise, checking a theorem proves a proposition in the specified definitions; it does not validate an economic application whose assumptions differ from those definitions.

Scope and preparation provenance

The formal artifact covers finite normalized real-valued characteristic functions and the specified four-axiom characterization. It does not formalize infinite-player games, nontransferable utility, a general permutation-average theorem, computational complexity, numerical approximation, or application-specific guarantees for attribution methods. The Shapley formula and associated constructions are marked noncomputable; finite mathematical sums are not presented here as an extracted executable implementation.

The pinned source metadata reports AI-assisted proof engineering with gpt-6-luna(Code xCLI). That historical disclosure concerns the formal development. This manuscript was prepared with GPT-6.1 assistance and its text is primarily AI-generated. The submitting contributor reports some human understanding of its content. These statements do not assert that every listed manuscript author personally reviewed every proof term. The independent source and mathematical review and the document checks have the limited scope stated above.

The Lean repository remains licensed BSD-3-Clause. The CC BY 4.0 license of this newly written manuscript is separate and does not relicense the repository. No source-repository change or new registry verification is implied by preparation of this exposition.

References