{"id":"palomar/PALOMAR-2026-10-01-000004","url":"https://github.com/Arthur742Ramos/minimax-theorem-lean/tree/0d5e3fd6ec3d56f5cafa34886019c46668fcf9ff","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-01-000004-v1.json","repo":"https://github.com/Arthur742Ramos/minimax-theorem-lean","tags":["cs.GT","math.OC","msc:91A05","game-theory","minimax","lean","formalization"],"score":0,"title":"minimax-theorem-lean","trust":"high","domain":"cs.GT","source":"palomar","authors":["Arthur Freitas Ramos"],"reviews":0,"subject":"cs.GT","summary":"A Lean formalization of von Neumann's 1928 finite two-player zero-sum minimax theorem, a foundation of modern game theory and a cornerstone of mathematical economics. Nash equilibrium existence builds directly on its mixed-strategy solution concept by extending equilibrium existence beyond the two-player zero-sum case; this is historical motivation, not a claimed Lean proof of Nash's theorem. The formal result is Minimax.minimax_theorem {A B : Type*} [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (u : A → B → ℝ) : maxminValue u = minmaxValue u. The reported Palomar registry API search on…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"verified":true,"discussed":0,"published":"2026-10-01","reactions":{},"formalized":true,"formalizes":[{"title":"Zur Theorie der Gesellschaftsspiele","identifier":"","relationship":"formalizes"}]}