@article{Nash1950,
  author = {Nash, Jr., John F.},
  title = {The Bargaining Problem},
  journal = {Econometrica},
  year = {1950},
  volume = {18},
  number = {2},
  pages = {155--162},
  doi = {10.2307/1907266},
  note = {\url{https://doi.org/10.2307/1907266}}
}
@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},
  pages = {367--381},
  publisher = {ACM},
  year = {2020},
  doi = {10.1145/3372885.3373824},
  note = {\url{https://doi.org/10.1145/3372885.3373824}}
}
@misc{BargainingArtifact,
  author = {Ramos, Arthur Freitas},
  title = {{Nash} Bargaining Solution Axiomatic Characterization},
  year = {2026},
  howpublished = {Lean 4 source repository, immutable commit \nolinkurl{0ddaa4bb858fa6fdf78074459eafada5e7938727}},
  note = {\url{https://github.com/Arthur742Ramos/nash-bargaining-lean/tree/0ddaa4bb858fa6fdf78074459eafada5e7938727}}
}
@misc{PalomarBargaining,
  author = {{Palomar Registry}},
  title = {{Nash} Bargaining Solution Axiomatic Characterization},
  year = {2026},
  howpublished = {PALOMAR-2026-09-25-000013, version 1, registered September 25, 2026},
  note = {\url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000013\&version=1}}
}