HEXAGONbeta

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

Primarily AI-generated textHuman understanding: some partsmath.LO — Logiccs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, inspection of the pinned source, exposition, source alignment, and bibliography and consistency review. Pinned formalization metadata separately records gpt-6-luna (Codex CLI) for historical proof engineering. Palomar records historical Lean, con-ron, and NanoDa acceptance for the exact registered source revision. No fresh Lean or independent-kernel run was performed during manuscript preparation. The paper distinguishes the registry challenge from the implemented solution, and does not claim every listed author has reviewed every proof term. This is an auditable exposition of an existing formalization of classical mathematics, with no claim of new mathematics or formalization priority.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion gpt-6-luna (historical proof engineering)
Lean
LeanVersion 4.35.0-rc2 (registered artifact)

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction–CADE 28, vol. 12699, pp. 625–635. 2021. \urlhttps://doi.org/10.1007/978-3-030-79876-5_37DOI
  2. Palomar Registry. Mechanical Verification of the Shapley Characterization. 2026. Verified September 24, 2026. \urlhttps://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36005001365
  3. Palomar Registry. Shapley Value Axiomatic Characterization. 2026. Registered September 25, 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000008&version=1
  4. Ramos, Arthur Freitas. Shapley Value Axiomatic Characterization in Lean 4. 2026. Commit \nolinkurlee15891fecdf294363791c61a5ec018109fe423a. \urlhttps://github.com/Arthur742Ramos/shapley-value-lean/tree/ee15891fecdf294363791c61a5ec018109fe423a
  5. Rota, Gian-Carlo. On the Foundations of Combinatorial Theory I. Theory of Mobius Functions. Zeitschrift fur Wahrscheinlichkeitstheorie und Verwandte Gebiete, vol. 2, pp. 340–368. 1964. \urlhttps://doi.org/10.1007/BF00531932DOI
  6. The Shapley Value: Essays in Honor of Lloyd S. Shapley. Cambridge University Press. 1988. \urlhttps://doi.org/10.1017/CBO9780511528446DOI
  7. Shapley, Lloyd S. A Value for n-Person Games. Contributions to the Theory of Games II, vol. 28. 1953. \urlhttps://doi.org/10.1515/9781400881970-018DOI
  8. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI

Version history

  1. v1Initial depositCurrentOct 01, 2026