HEXAGONbeta

Nash Bargaining Characterization in Lean

Primarily AI-generated textHuman understanding: some partsmath.LO — Logiccs.LO — Logic in Computer Science

Contributed by Arthur ↗, David Barros Hulak ↗, Ruy J. G. B. de Queiroz ↗

SubmitterArthur

Version 1 / Oct 01, 2026 / CC BY 4.0

Abstract

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 selection rules. We explain the algebraic midpoint proof of uniqueness and the normalization argument, including an explicit small-step tangent bound and a compact symmetric enlargement. The exposition is tied to an immutable repository snapshot and four declarations registered in Palomar. Historical registry verification is distinguished from the source inspection used to prepare this manuscript. The contribution is a documented formalization of established mathematics; no new bargaining theorem or formalization-priority claim is made.

Provenance statement

The manuscript names Arthur Freitas Ramos (submitting contributor; ORCID 0009-0003-3568-0325), David Barros Hulak (0009-0002-8056-1774), and Ruy J. G. B. de Queiroz (0000-0003-1482-0977). The submitting contributor reports understanding some parts, but not all, of the work. OpenAI GPT-6.1 assisted with manuscript drafting, pinned source inspection, exposition, bibliography, and consistency checks. Historical pinned formalization metadata separately records gpt-6-luna (Codex CLI) proof engineering. Registry verification is historical evidence for the exact source revision; no fresh Lean, Comparator, or independent-kernel run is claimed during manuscript preparation. The manuscript is a source-grounded exposition of the classical two-person Nash bargaining characterization, including four registered declarations. No new bargaining theorem or formalization-priority claim is made, and no complete independent human reconstruction or line-by-line validation by all authors is asserted.
FormalizationsPalomar

Tools used

OpenAI
ChatGPTVersion GPT 6.1 (manuscript)
OpenAI
CodexVersion gpt-6-luna (historical proof engineering)
Lean
LeanVersion 4.35.0-rc2 (registered artifact)

References

  1. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction–CADE 28, vol. 12699, pp. 625–635. 2021. \urlhttps://doi.org/10.1007/978-3-030-79876-5_37DOI
  2. Nash, Jr., John F. The Bargaining Problem. Econometrica, vol. 18, no. 2, pp. 155–162. 1950. \urlhttps://doi.org/10.2307/1907266DOI
  3. Palomar Registry. Nash Bargaining Solution Axiomatic Characterization. 2026. \urlhttps://palomar-registry.org/entry?id=PALOMAR-2026-09-25-000013&version=1
  4. Ramos, Arthur Freitas. Nash Bargaining Solution Axiomatic Characterization. 2026. \urlhttps://github.com/Arthur742Ramos/nash-bargaining-lean/tree/0ddaa4bb858fa6fdf78074459eafada5e7938727
  5. The mathlib Community. The Lean Mathematical Library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 367–381. 2020. \urlhttps://doi.org/10.1145/3372885.3373824DOI

Version history

  1. v1Initial depositCurrentOct 01, 2026