@article{vonNeumann1928,
  author = {von Neumann, John},
  title = {{Zur Theorie der Gesellschaftsspiele}},
  journal = {Mathematische Annalen},
  volume = {100},
  pages = {295--320},
  year = {1928},
  doi = {10.1007/BF01448847},
  note = {\url{https://doi.org/10.1007/BF01448847}}
}
@article{Sion1958,
  author = {Sion, Maurice},
  title = {On general minimax theorems},
  journal = {Pacific Journal of Mathematics},
  volume = {8},
  number = {1},
  pages = {171--176},
  year = {1958},
  doi = {10.2140/pjm.1958.8.171},
  note = {\url{https://doi.org/10.2140/pjm.1958.8.171}}
}
@article{Komiya1988,
  author = {Komiya, Hidetoshi},
  title = {Elementary proof for {Sion}'s minimax theorem},
  journal = {Kodai Mathematical Journal},
  volume = {11},
  number = {1},
  pages = {5--7},
  year = {1988},
  doi = {10.2996/kmj/1138038812},
  note = {\url{https://doi.org/10.2996/kmj/1138038812}}
}
@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},
  year = {2020},
  pages = {367--381},
  publisher = {ACM},
  doi = {10.1145/3372885.3373824},
  note = {\url{https://arxiv.org/abs/1910.09336}}
}
@misc{MathlibSion,
  author = {Chambert-Loir, Antoine and Dedecker, Anatole},
  title = {Formalization of {Sion}'s version of the von {Neumann} minimax theorem},
  year = {2025},
  howpublished = {Mathlib 4, \texttt{Mathlib/Topology/Sion.lean}},
  note = {Pinned revision \nolinkurl{065356127b1dc0016f66b7283ce0ce2c4055aa55}, accessed September 30, 2026. \url{https://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/Topology/Sion.lean}}
}
@misc{MinimaxArtifact,
  author = {Ramos, Arthur Freitas},
  title = {Von {Neumann}'s minimax theorem in {Lean}},
  year = {2026},
  howpublished = {Version-pinned source repository},
  note = {Revision \nolinkurl{f1d1d00591548c174407cd59ddc623a461c082c1}, accessed September 30, 2026. \url{https://github.com/Arthur742Ramos/minimax-theorem-lean/tree/f1d1d00591548c174407cd59ddc623a461c082c1}}
}
@misc{VerificationRun,
  author = {{PalomarRegistry}},
  title = {Verification workflow for the minimax submission},
  year = {2026},
  howpublished = {Workflow run 36719764602},
  note = {Mechanical report checked September 30, 2026, for source revision \nolinkurl{f1d1d00591548c174407cd59ddc623a461c082c1}. \url{https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36719764602}}
}