@incollection{shapley1953,
  author = {Shapley, Lloyd S.},
  title = {A Value for n-Person Games},
  booktitle = {Contributions to the Theory of Games II},
  editor = {Kuhn, Harold W. and Tucker, Albert W.},
  series = {Annals of Mathematics Studies},
  volume = {28},
  publisher = {Princeton University Press},
  year = {1953},
  doi = {10.1515/9781400881970-018},
  note = {\url{https://doi.org/10.1515/9781400881970-018}}
}
@book{roth1988,
  editor = {Roth, Alvin E.},
  title = {The {Shapley} Value: Essays in Honor of {Lloyd S. Shapley}},
  publisher = {Cambridge University Press},
  year = {1988},
  doi = {10.1017/CBO9780511528446},
  note = {\url{https://doi.org/10.1017/CBO9780511528446}}
}
@article{rota1964,
  author = {Rota, Gian-Carlo},
  title = {On the Foundations of Combinatorial Theory {I}. Theory of {M\"obius} Functions},
  journal = {Zeitschrift f\"ur Wahrscheinlichkeitstheorie und Verwandte Gebiete},
  volume = {2},
  pages = {340--368},
  year = {1964},
  doi = {10.1007/BF00531932},
  note = {\url{https://doi.org/10.1007/BF00531932}}
}
@inproceedings{lean4,
  author = {de Moura, Leonardo and Ullrich, Sebastian},
  title = {The {Lean} 4 Theorem Prover and Programming Language},
  booktitle = {Automated Deduction---CADE 28},
  series = {Lecture Notes in Computer Science},
  volume = {12699},
  pages = {625--635},
  publisher = {Springer},
  year = {2021},
  doi = {10.1007/978-3-030-79876-5_37},
  note = {\url{https://doi.org/10.1007/978-3-030-79876-5_37}}
}
@inproceedings{mathlib2020,
  author = {{The mathlib Community}},
  title = {The {Lean} Mathematical Library},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  series = {CPP 2020},
  pages = {367--381},
  publisher = {ACM},
  year = {2020},
  doi = {10.1145/3372885.3373824},
  note = {\url{https://doi.org/10.1145/3372885.3373824}}
}
@misc{ramos2026,
  author = {Ramos, Arthur Freitas},
  title = {{Shapley} Value Axiomatic Characterization in {Lean} 4},
  year = {2026},
  howpublished = {Source repository, registered revision},
  note = {Commit \nolinkurl{ee15891fecdf294363791c61a5ec018109fe423a}.
  \url{https://github.com/Arthur742Ramos/shapley-value-lean/tree/ee15891fecdf294363791c61a5ec018109fe423a}}
}
@misc{palomar2026,
  author = {{Palomar Registry}},
  title = {{Shapley} Value Axiomatic Characterization},
  year = {2026},
  howpublished = {Registered formalization, PALOMAR-2026-09-25-000008, version 1},
  note = {Registered September 25, 2026.
  \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000008&version=1}}
}
@misc{verification2026,
  author = {{Palomar Registry}},
  title = {Mechanical Verification of the {Shapley} Characterization},
  year = {2026},
  howpublished = {GitHub Actions workflow run 36005001365},
  note = {Verified September 24, 2026. \url{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36005001365}}
}