{"id":"palomar/PALOMAR-2026-10-02-000005","url":"https://github.com/Arthur742Ramos/maskin-nash-implementation-lean/tree/9c041756dcee8e572b73f4c12b62e6c95322db09","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-02-000005-v1.json","repo":"https://github.com/Arthur742Ramos/maskin-nash-implementation-lean","tags":["cs.GT","econ.TH","msc:91B26","mechanism-design","game-theory","lean-formalization"],"score":0,"title":"maskin-nash-implementation-lean","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"cs.GT","summary":"Lean 4 formalization of Maskin's theorem on Nash implementation: necessity of Maskin monotonicity and sufficiency of monotonicity plus no-veto power via the canonical mechanism. Alternatives form a finite nonempty type, agents are indexed by Fin n, preferences are complete preorders, and the social choice correspondence is nonempty-valued. Sufficiency requires at least three agents; implementation is in pure strategies.","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-02","reactions":{},"formalized":true,"formalizes":[{"title":"Nash Equilibrium and Welfare Optimality","identifier":"","relationship":"formalizes"}]}