{"id":"hexagon/2610.00005","pdf":"https://hexagonmath.org/pdf/2610.00005v1","url":"https://hexagonmath.org/abs/2610.00005v1","tags":["cs.LO","msc:91A12","msc:68V20"],"score":0,"title":"Nash Bargaining Characterization in Lean","domain":"math.LO","origin":"ai-generated","source":"hexagon","authors":["Arthur","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.LO","summary":"We describe a Lean 4 formalization of the classical two-person Nash bargaining characterization. A bargaining problem consists of a compact convex subset of the real plane, a feasible disagreement point, and a feasible outcome strictly improving both utilities. The Nash product is maximized over the individually rational part of that set. The development proves existence and uniqueness of the maximizer, verifies Pareto optimality, symmetry, positive affine invariance, and independence of irrelevant alternatives, and proves that these four axioms characterize the maximizer among feasible…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"ai_models":["ChatGPT","Codex"],"discussed":0,"published":"2026-10-01","reactions":{},"withdrawn":false,"authorship":"no-human-author-claimed","formalized":true,"formalizations":["https://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000013&version=1"],"human_understanding":"some"}