{"id":"palomar/PALOMAR-2026-09-07-000014","url":"https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean/tree/2f65710af26a24a26660dd1e92d09adf1697a527","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000014-v1.json","repo":"https://github.com/Arthur742Ramos/dependent-nash-equilibrium-lean","tags":["math.LO","cs.LO","msc:91A10","game-theory","nash-equilibrium","lean","formalization"],"score":0,"title":"Dependent finite mixed Nash equilibria in Lean","trust":"high","domain":"math.LO","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"math.LO","summary":"A Lean-native formalization of finite mixed Nash equilibrium for games in which each player has its own finite, nonempty action type. The library defines dependent profiles and finite expected payoffs, proves support equalization and Dirac transport, establishes the closed/compact/convex mixed-profile geometry, and connects the normalized excess map to a checked product-of-simplices Brouwer theorem. It also proves the correspondence between ambient finite games with player-indexed legal action sets and dependent legal-action subtypes. This is a reusable formalization artifact, not a claim of…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-07","reactions":{},"formalized":true,"formalizes":[{"title":"Equilibrium points in n-person games","identifier":"https://doi.org/10.1073/pnas.36.1.48","relationship":"formalizes"},{"title":"Formalizing Scarf, Brouwer, and Nash in Lean","identifier":"https://arxiv.org/abs/2607.05987","relationship":"adapts"}]}