HEXAGONbeta

A Lean Formalization of Finite Zero Sum Minimax via Sion's Theorem

Primarily AI-generated textHuman understanding: some partsmath.OC — Optimization and Controlcs.LO — Logic in Computer Sciencecs.MS — Mathematical Software

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

SubmitterArthur

Version 1 / Sep 30, 2026 / CC BY 4.0

Abstract

We describe a Lean 4 formalization of the minimax theorem for finite nonempty two-player zero-sum games with arbitrary real payoffs. Mixed strategies are probability vectors, and the two game values are defined using real indexed suprema and infima. An explicit payoff bound supplies the boundedness obligations required by these conditional extrema. The reverse minimax inequality follows by applying Mathlib's proved Sion saddle-point theorem to compact convex coordinate simplices, with the minimizing player placed in its first argument. We explain the representation bridge, the proof obligations, and the passage from a saddle point to equality. The accompanying version-pinned artifact separates a reusable library from a statement-only challenge and its proved solution. This is an exposition of a finite-game specialization of existing formal analysis, with no claim of a new mathematical proof or formalization priority.

Provenance statement

AI assistance from GPT-6.1 was used for formalization and packaging, as disclosed in the artifact metadata, and for preparation of this exposition. The manuscript describes the pinned public Lean artifact at https://github.com/Arthur742Ramos/minimax-theorem-lean/tree/f1d1d00591548c174407cd59ddc623a461c082c1. The proof specializes Mathlib's existing Sion theorem. Automated checks establish the formal artifact conclusions; they do not establish a level of human understanding. The submitting contributor reports that some parts have been checked and understood by a human.

Tools used

Lean
LeanVersion 4.35.0-rc2
OpenAI
CodexVersion GPT-6.1

References

  1. Chambert-Loir, Antoine; Dedecker, Anatole. Formalization of Sion's version of the von Neumann minimax theorem. 2025. Pinned revision \nolinkurl065356127b1dc0016f66b7283ce0ce2c4055aa55, accessed September 30, 2026. \urlhttps://github.com/leanprover-community/mathlib4/blob/065356127b1dc0016f66b7283ce0ce2c4055aa55/Mathlib/Topology/Sion.lean
  2. Komiya, Hidetoshi. Elementary proof for Sion's minimax theorem. Kodai Mathematical Journal, vol. 11, no. 1, pp. 5–7. 1988. \urlhttps://doi.org/10.2996/kmj/1138038812DOI
  3. PalomarRegistry. Verification workflow for the minimax submission. 2026. Mechanical report checked September 30, 2026, for source revision \nolinkurlf1d1d00591548c174407cd59ddc623a461c082c1. \urlhttps://github.com/PalomarRegistry/PalomarSubmission/actions/runs/36719764602
  4. Ramos, Arthur Freitas. Von Neumann's minimax theorem in Lean. 2026. Revision \nolinkurlf1d1d00591548c174407cd59ddc623a461c082c1, accessed September 30, 2026. \urlhttps://github.com/Arthur742Ramos/minimax-theorem-lean/tree/f1d1d00591548c174407cd59ddc623a461c082c1
  5. Sion, Maurice. On general minimax theorems. Pacific Journal of Mathematics, vol. 8, no. 1, pp. 171–176. 1958. \urlhttps://doi.org/10.2140/pjm.1958.8.171DOI
  6. 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://arxiv.org/abs/1910.09336DOI
  7. von Neumann, John. Zur Theorie der Gesellschaftsspiele. Mathematische Annalen, vol. 100, pp. 295–320. 1928. \urlhttps://doi.org/10.1007/BF01448847DOI

Version history

  1. v1Initial depositCurrentSep 30, 2026