{"id":"palomar/PALOMAR-2026-09-07-000009","url":"https://github.com/Arthur742Ramos/nash-equilibrium-lean/tree/6dd83f3b004c0318e52f4c3cb272d909efca321d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-07-000009-v1.json","repo":"https://github.com/Arthur742Ramos/nash-equilibrium-lean","tags":["math.LO","cs.LO","msc:91A10","game-theory","nash-equilibrium","lean-formalization"],"score":0,"title":"Native Lean finite Nash equilibria","trust":"high","domain":"math.LO","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"math.LO","summary":"Formalizes finite strategic-form games with player-specific finite move sets, pure profiles, unilateral deviations, best responses, dominant strategies, and two distinct potential notions. Pure Nash equilibrium is defined over utility preorders by the absence of a strict improvement; weak-inequality characterizations are restricted to linear orders. The library names the one-way improvement condition a generalized ordinal potential and reserves ordinal potential for the standard bidirectional strict-sign condition. It proves a global potential-maximizer certificate for pure Nash equilibrium,…","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":"Potential Games","identifier":"https://doi.org/10.1006/game.1996.0044","relationship":"formalizes"},{"title":"Formalizing Scarf, Brouwer, and Nash in Lean","identifier":"https://arxiv.org/abs/2607.05987","relationship":"adapts"}]}