% Verified metadata with printable source links.

@article{Nash1950,
  author = {Nash, Jr., John F.},
  title = {Equilibrium Points in {n}-Person Games},
  journal = {Proceedings of the National Academy of Sciences of the United States of America},
  year = {1950},
  month = jan,
  volume = {36},
  number = {1},
  pages = {48--49},
  doi = {10.1073/pnas.36.1.48},
  url = {https://doi.org/10.1073/pnas.36.1.48},
  note = {DOI: \href{https://doi.org/10.1073/pnas.36.1.48}{\nolinkurl{10.1073/pnas.36.1.48}}}
}

@article{Nash1951,
  author = {John Nash},
  title = {Non-Cooperative Games},
  journal = {Annals of Mathematics},
  year = {1951},
  month = sep,
  volume = {54},
  number = {2},
  pages = {286--295},
  doi = {10.2307/1969529},
  url = {https://www.jstor.org/stable/1969529},
  note = {DOI: \href{https://doi.org/10.2307/1969529}{\nolinkurl{10.2307/1969529}}}
}

@article{PotentialGames,
  author = {Dov Monderer and Lloyd S. Shapley},
  title = {Potential Games},
  journal = {Games and Economic Behavior},
  year = {1996},
  month = may,
  volume = {14},
  number = {1},
  pages = {124--143},
  doi = {10.1006/game.1996.0044},
  url = {https://www.sciencedirect.com/science/article/pii/S0899825696900445},
  note = {DOI: \href{https://doi.org/10.1006/game.1996.0044}{\nolinkurl{10.1006/game.1996.0044}}}
}

@article{AFPNash,
  author = {Arthur Freitas Ramos and David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz},
  title = {{Nash} Equilibria for Finite Games in {Isabelle/HOL}},
  journal = {Archive of Formal Proofs},
  year = {2026},
  month = may,
  date = {2026-05-07},
  issn = {2150-914X},
  note = {Formal proof development; \url{https://isa-afp.org/entries/Nash_Equilibrium.html}},
  url = {https://isa-afp.org/entries/Nash_Equilibrium.html},
  urldate = {2026-10-01}
}

@misc{LyuLi2026,
  author = {Yuwei Lyu and Kai Li},
  title = {Formalizing {Scarf}, {Brouwer}, and {Nash} in {Lean}},
  year = {2026},
  month = jul,
  date = {2026-07-07},
  eprint = {2607.05987},
  archivePrefix = {arXiv},
  primaryClass = {cs.LO},
  doi = {10.48550/arXiv.2607.05987},
  url = {https://arxiv.org/abs/2607.05987v1},
  note = {Version 1; arXiv: \href{https://arxiv.org/abs/2607.05987v1}{2607.05987v1}; DOI: \href{https://doi.org/10.48550/arXiv.2607.05987}{\nolinkurl{10.48550/arXiv.2607.05987}}}
}

@misc{BrouwerSource,
  author = {{Math\_XMUM}},
  title = {Game Theory Formalization in {Lean}},
  year = {2026},
  howpublished = {GitHub repository},
  url = {https://github.com/math-xmum/Brouwer/tree/09941e849a81e520cc0cc53220f10f8e5f4768e0},
  note = {Commit \nolinkurl{09941e849a81e520cc0cc53220f10f8e5f4768e0}; MIT License; \url{https://github.com/math-xmum/Brouwer/tree/09941e849a81e520cc0cc53220f10f8e5f4768e0}},
  urldate = {2026-10-01}
}

@inproceedings{Lean4,
  author = {Leonardo de Moura and Sebastian Ullrich},
  title = {The {Lean 4} Theorem Prover and Programming Language},
  booktitle = {Automated Deduction -- CADE 28},
  editor = {Andr{\'e} Platzer and Geoff Sutcliffe},
  series = {Lecture Notes in Computer Science},
  volume = {12699},
  year = {2021},
  pages = {625--635},
  publisher = {Springer},
  address = {Cham},
  doi = {10.1007/978-3-030-79876-5_37},
  url = {https://link.springer.com/chapter/10.1007/978-3-030-79876-5_37},
  note = {DOI: \href{https://doi.org/10.1007/978-3-030-79876-5_37}{\nolinkurl{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},
  year = {2020},
  pages = {367--381},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  doi = {10.1145/3372885.3373824},
  url = {https://doi.org/10.1145/3372885.3373824},
  note = {DOI: \href{https://doi.org/10.1145/3372885.3373824}{\nolinkurl{10.1145/3372885.3373824}}}
}

@article{Bagnall2017,
  author = {Alexander Bagnall and Samuel Merten and Gordon Stewart},
  title = {A Library for Algorithmic Game Theory in {Ssreflect/Coq}},
  journal = {Journal of Formalized Reasoning},
  year = {2017},
  volume = {10},
  number = {1},
  pages = {67--95},
  doi = {10.6092/issn.1972-5787/7235},
  url = {https://jfr.unibo.it/article/view/7235},
  note = {DOI: \href{https://doi.org/10.6092/issn.1972-5787/7235}{\nolinkurl{10.6092/issn.1972-5787/7235}}}
}

@misc{NativeArtifact,
  author = {Arthur Freitas Ramos},
  title = {Native {Lean} finite {Nash} equilibria},
  year = {2026},
  howpublished = {GitHub repository},
  url = {https://github.com/Arthur742Ramos/nash-equilibrium-lean/tree/6dd83f3b004c0318e52f4c3cb272d909efca321d},
  note = {Commit \nolinkurl{6dd83f3b004c0318e52f4c3cb272d909efca321d}; native sources BSD-3-Clause, vendored fixed-point sources MIT; \url{https://github.com/Arthur742Ramos/nash-equilibrium-lean/tree/6dd83f3b004c0318e52f4c3cb272d909efca321d}},
  urldate = {2026-10-01}
}

@misc{DependentArtifact,
  author = {Arthur Freitas Ramos},
  title = {Dependent finite mixed {Nash} equilibria in {Lean}},
  year = {2026},
  howpublished = {GitHub repository},
  url = {https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/tree/2f65710af26a24a26660dd1e92d09adf1697a527},
  note = {Commit \nolinkurl{2f65710af26a24a26660dd1e92d09adf1697a527}; native sources BSD-3-Clause, vendored fixed-point sources MIT; \url{https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/tree/2f65710af26a24a26660dd1e92d09adf1697a527}},
  urldate = {2026-10-01}
}

@misc{PalomarNative,
  author = {Arthur Freitas Ramos},
  title = {Native {Lean} finite {Nash} equilibria},
  year = {2026},
  month = sep,
  date = {2026-09-07},
  howpublished = {Palomar Registry},
  note = {PALOMAR-2026-09-07-000009, version 1; \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000009&version=1}},
  url = {https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000009&version=1},
  urldate = {2026-10-01}
}

@misc{PalomarDependent,
  author = {Arthur Freitas Ramos},
  title = {Dependent finite mixed {Nash} equilibria in {Lean}},
  year = {2026},
  month = sep,
  date = {2026-09-07},
  howpublished = {Palomar Registry},
  note = {PALOMAR-2026-09-07-000014, version 1; \url{https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000014&version=1}},
  url = {https://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000014&version=1},
  urldate = {2026-10-01}
}