HEXAGONbeta

Finite Nash Equilibria and Dependent Mixed Strategies in Lean

Primarily AI-generated textHuman understanding: some partsmath.LO — Logiccs.LO — Logic in Computer Sciencecs.MS — Mathematical Software

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

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

We present two complementary Lean 4 developments of finite Nash equilibrium. The pure-game layer uses player-specific legal action sets, distinguishes one-way generalized ordinal potentials from bidirectional ordinal potentials, and proves potential-maximizer certificates, a local-maximum characterization, absence of strict-improvement cycles, and weak acyclicity. The mixed-game layers use either a common finite action type or a dependent finite action type for each player. They prove payoff equalization on equilibrium supports, Dirac payoff identities, continuity of the normalized payoff-excess map, and mixed equilibrium existence. We explain the finite-sum and sum-of-squares arguments and the reindexing bridge to an attributed, proved product-of-simplices Brouwer theorem. An additional legal-subtype interface is separated from the declarations selected by the registry comparator. The account is tied to two immutable source snapshots and dated verification records. It documents established mathematics and its formal interfaces, without claiming a new equilibrium theorem or formalization priority.

Provenance statement

This manuscript was primarily drafted with OpenAI GPT-6.1 under author direction, including exposition, pinned-source comparison, bibliographic research and typesetting. The submitting contributor Arthur Freitas Ramos reports understanding some parts. No complete independent human reconstruction or line-by-line human validation of every formal proof is claimed. The two historical Lean artifacts separately record GPT-5 Codex proof-engineering assistance. The native source is pinned at 6dd83f3b004c0318e52f4c3cb272d909efca321d in https://github.com/Arthur742Ramos/nash-equilibrium-lean and the dependent source at 2f65710af26a24a26660dd1e92d09adf1697a527 in https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean. The exposition consolidates PALOMAR-2026-09-07-000009 v1 and PALOMAR-2026-09-07-000014 v1, explicitly separating selected declarations from the additional legal-subtype interface. It attributes classical Nash and potential-game results, prior AFP and Coq formalizations, and the reused Lyu-Li product-of-simplices fixed-point infrastructure. No new mathematical theorem or formalization priority is claimed. Historical verification records use Lean 4.33.0 and Mathlib db584cd6d46c92f209a44c0f1c829460d327499d; no fresh Lean build or external checker rerun was performed during manuscript preparation. Pinned sources, registry Challenge/Solution hashes, comparator boundaries and attribution were inspected. Independent AI-assisted mathematical, source-alignment and bibliography reviews cleared the manuscript; this is not human peer review. The eight-page LaTeX PDF was compiled and every page visually inspected, and the source-only ZIP was extracted and cleanly rebuilt. Manuscript and TeX/Bib source are CC BY 4.0; the Lean projects retain BSD-3-Clause and the included fixed-point files retain MIT. The manuscript byline does not alter the registry attribution to Arthur as formalization author and responsible maintainer.
FormalizationsPalomarPalomar

Tools used

Lean
LeanVersion 4.33.0 (historical pinned proofs)
OpenAI
CodexVersion GPT-6.1 (manuscript)

References

  1. Alexander Bagnall; Samuel Merten; Gordon Stewart. A Library for Algorithmic Game Theory in Ssreflect/Coq. Journal of Formalized Reasoning, vol. 10, no. 1, pp. 67–95. 2017. DOI: \hrefhttps://doi.org/10.6092/issn.1972-5787/7235\nolinkurl10.6092/issn.1972-5787/7235DOI
  2. Leonardo de Moura; Sebastian Ullrich. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021. DOI: \hrefhttps://doi.org/10.1007/978-3-030-79876-5_37\nolinkurl10.1007/978-3-030-79876-5_37DOI
  3. Yuwei Lyu; Kai Li. Formalizing Scarf, Brouwer, and Nash in Lean. 2026. Version 1; arXiv: \hrefhttps://arxiv.org/abs/2607.05987v12607.05987v1; DOI: \hrefhttps://doi.org/10.48550/arXiv.2607.05987\nolinkurl10.48550/arXiv.2607.05987arXivDOI
  4. Math_XMUM. Game Theory Formalization in Lean. 2026. Commit \nolinkurl09941e849a81e520cc0cc53220f10f8e5f4768e0; MIT License; \urlhttps://github.com/math-xmum/Brouwer/tree/09941e849a81e520cc0cc53220f10f8e5f4768e0link
  5. Dov Monderer; Lloyd S. Shapley. Potential Games. Games and Economic Behavior, vol. 14, no. 1, pp. 124–143. 1996. DOI: \hrefhttps://doi.org/10.1006/game.1996.0044\nolinkurl10.1006/game.1996.0044DOI
  6. John Nash. Non-Cooperative Games. Annals of Mathematics, vol. 54, no. 2, pp. 286–295. 1951. DOI: \hrefhttps://doi.org/10.2307/1969529\nolinkurl10.2307/1969529DOI
  7. Nash, Jr., John F. Equilibrium Points in n-Person Games. Proceedings of the National Academy of Sciences of the United States of America, vol. 36, no. 1, pp. 48–49. 1950. DOI: \hrefhttps://doi.org/10.1073/pnas.36.1.48\nolinkurl10.1073/pnas.36.1.48DOI
  8. Arthur Freitas Ramos. Dependent finite mixed Nash equilibria in Lean. 2026. Commit \nolinkurl2f65710af26a24a26660dd1e92d09adf1697a527; native sources BSD-3-Clause, vendored fixed-point sources MIT; \urlhttps://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/tree/2f65710af26a24a26660dd1e92d09adf1697a527link
  9. Arthur Freitas Ramos. Dependent finite mixed Nash equilibria in Lean. 2026. PALOMAR-2026-09-07-000014, version 1; \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000014&version=1link
  10. Arthur Freitas Ramos. Native Lean finite Nash equilibria. 2026. Commit \nolinkurl6dd83f3b004c0318e52f4c3cb272d909efca321d; native sources BSD-3-Clause, vendored fixed-point sources MIT; \urlhttps://github.com/Arthur742Ramos/nash-equilibrium-lean/tree/6dd83f3b004c0318e52f4c3cb272d909efca321dlink
  11. Arthur Freitas Ramos. Native Lean finite Nash equilibria. 2026. PALOMAR-2026-09-07-000009, version 1; \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-07-000009&version=1link
  12. Arthur Freitas Ramos; David Barros Hulak; Ruy Jose Guerra Barretto de Queiroz. Nash Equilibria for Finite Games in Isabelle/HOL. Archive of Formal Proofs. 2026. Formal proof development; \urlhttps://isa-afp.org/entries/Nash_Equilibrium.htmllink
  13. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. DOI: \hrefhttps://doi.org/10.1145/3372885.3373824\nolinkurl10.1145/3372885.3373824DOI

Version history

  1. v1Initial depositCurrentOct 01, 2026