Nash Bargaining Characterization in Lean

The result and its scope

Nash’s bargaining solution selects a cooperative outcome by maximizing the product of the players’ utility gains above disagreement. His 1950 paper gives an axiomatic justification for this choice [2]. The mathematical question is distinct from the existence of a Nash equilibrium in a noncooperative game: here the input is a feasible utility set and a disagreement point, and the output is one utility pair.

This article explains the development Arthur742Ramos/nash-bargaining-lean at commit 0ddaa4bb858fa6fdf78074459eafada5e7938727 [4]. The selected declarations are registered as PALOMAR-2026-09-25-000013, version 1 [3]. The formalization uses Lean 4 and Mathlib [1, 5]. References to source files below always mean this pinned snapshot, rather than a moving branch.

The scope is precisely two players with real-valued utilities. Feasible sets are compact and convex, disagreement is feasible, and a strictly mutually beneficial outcome exists. No comprehensiveness or downward closure of the feasible set is assumed. The feasible set may contain outcomes below disagreement. The theorem concerns a utility-space selection rule; it does not construct a bargaining protocol, prove strategic implementation, or supply an executable optimization algorithm.

The formalization’s useful content lies in making this domain explicit and carrying it through both directions of the characterization. Its proof separates compactness-based attainment from algebraic uniqueness, and gives a direct real-arithmetic version of the normalization argument. These are implementation and exposition contributions for a classical result, not claims of a new solution concept.

2020 Mathematics Subject Classification. 91A12, 68V20.

Author ORCID identifiers: Arthur Freitas Ramos, 0009-0003-3568-0325; David Barros Hulak, 0009-0002-8056-1774; Ruy J. G. B. de Queiroz, 0000-0003-1482-0977.

Copyright 2026 the authors. Licensed under Creative Commons Attribution 4.0 International (CC BY 4.0).

Bargaining problems and individual rationality

Definition 2.1. A problem is a pair $P=(S,d)$ such that $S \subseteq\mathbb{R}^{2}$ is nonempty, compact, and convex, $d \in S$, and

Write $\mathcal{B}$ for this class of problems. Its individually rational part is

The Nash product and maximizer predicate are

These definitions translate NashBargaining.Problem, nashProduct, and IsNashMaximizer in Basic.lean. The Lean type bundles the set and point with proofs of all five conditions in Definition 2.1. The nonempty condition is retained explicitly although it follows from $d \in S$.

The restriction to $\operatorname{IR}(P)$ is essential. For example, take $d=(0,0)$ and $S=\{(t,t):-2\le t\le1\}$. The raw product is $t^{2}$, whose maximum on $S$ is attained at $(-2,-2)$, whereas its maximum on $\operatorname{IR}(P)$ is attained at $(1,1)$. Thus a statement about maximization over all of $S$ would misdescribe the formal theorem, even for a compact convex problem satisfying (1).

Strict simultaneous improvement ensures that the maximum product is positive. It excludes the flat zero-product case: on $S=[0,1]\times\{0\}$ with $d=(0,0)$, every individually rational point has product zero, so uniqueness fails. A strictly improving point need not be an interior point of $S$ in the plane. The admissible diagonal segment in the preceding example already has empty planar interior.

Definition 2.2. A solution is a function $F:\mathcal{B}\to\mathbb{R}^{2}$ satisfying $F(S,d)\in S$ for every problem. No individual-rationality condition is included in the definition of a solution.

The corresponding Lean type NashBargaining.Solution is a subtype of functions with a feasibility proof. This matters for the converse: the characterization starts with any feasible rule satisfying the four axioms, rather than assuming in advance that it selects an individually rational point.

The four axioms

The predicates in Basic.lean have the following mathematical content. Every quantified problem below belongs to $\mathcal{B}$.

1. Pareto optimality. If $y\in S$ and $F(P)_{1}\le y_{1}$, $F(P)_{2}\le y_{2}$, then $y=F(P)$. This rules out weak domination with at least one strict utility gain.

2. Symmetry. Define $\operatorname{swap}(u_{1},u_{2})=(u_{2},u_{1})$. If $\operatorname{swap}(S)=S$ and $d_{1}=d_{2}$, then $F(P)_{1}=F(P)_{2}$. This is a condition on symmetric problems, not a separately assumed equivariance law for every permutation of an arbitrary problem.

3. Positive affine invariance. For

   $$A(u)=(a_{1}u_{1}+b_{1},a_{2}u_{2}+b_{2}),\qquad a_{1},a_{2}>0,$$

   if $Q=(A(S),A(d))$, then $F(Q)=A(F(P))$. Both the feasible set and disagreement point transform together; the two scales and translations may be different.

4. Independence of irrelevant alternatives (IIA). If $P=(S,d)$, $Q=(T,d)$, $S\subseteq T$, and $F(Q)\in S$, then $F(P)=F(Q)$. The smaller problem must remain in $\mathcal{B}$.

Their conjunction is NashBargaining.NashAxioms. In particular, IIA compares sets at the same disagreement point. It does not assert invariance under arbitrary changes to disagreement or contraction to sets outside the specified domain.

The formal theorem interface

Theorem 4.1. For every $P \in\mathcal{B}$ there exists exactly one $x \in\mathbb{R}^{2}$ such that $\operatorname{Max}(P,x)$. If a function $N$ selects a maximizer for every problem, its induced feasible solution satisfies the four axioms. Conversely, for every feasible solution $F$ satisfying the axioms, every $P \in\mathcal{B}$, and every $x$ with $\operatorname{Max}(P,x)$, one has $F(P)=x$.

The registered namespace is NashBargaining.Palomar. Its four declarations are:

• nashMaximizerExists: $\forall P,\ \exists x,\ \operatorname{Max}(P,x)$;

• nashMaximizerUnique: any two maximizers for one problem agree;

• nashSatisfiesAxioms: any pointwise maximizer selector satisfies the axioms;

• axiomsCharacterizeNash: an axiomatic feasible rule agrees with any given maximizer.

The registered declarations in Solution.lean are wrappers around implementation theorems in the main namespace. The existence and uniqueness assertions do not themselves define a particular selector. Classically, existence permits choosing one for each problem, and uniqueness makes all such selections extensionally equal. The axiom-verification theorem is deliberately expressed for an arbitrary function together with its pointwise maximizer proofs.

Attainment and algebraic uniqueness

Compactness gives a maximum

For $P=(S,d)$, let

The coordinate half-spaces are closed, so $K$ is compact. It is nonempty by (1). The map $u\mapsto\operatorname{NP}_{d}(u)$ is continuous as a product of two continuous coordinate differences. The extreme-value theorem therefore supplies a point of maximum on $K$.

In Existence.lean, attainment follows from Mathlib’s IsCompact.exists_isMaxOn theorem. The proof then unpacks membership in $K$ into feasibility and the two individual-rationality inequalities. Convexity is not used in this attainment step, although it remains part of the input type and is needed for uniqueness and characterization.

Positive product and a midpoint identity

Suppose $x,y$ both maximize. Put

The gains are initially nonnegative. Comparing each maximizer with the other gives $ab=ce=M$. Comparing with the strictly improving witness gives $M>0$, hence $a,b,c,e>0$.

If $a=c$, cancellation in $ab=ce$ gives $b=e$, so $x=y$. Otherwise, convexity places $z=(x+y)/2$ in $S$. It is individually rational, with gains $u=(a+c)/2$, $v=(b+e)/2$. The crucial equality is

It follows by expanding and substituting $ce=ab$. Its right side is strictly positive when $a\ne c$, while $4c>0$. Therefore $uv>M$, contradicting maximality of $x$.

This is the proof in Uniqueness.lean. It expresses strictness through a polynomial identity and positivity, without introducing logarithms, derivatives, or a strict-concavity library. The product function is not concave on the entire nonnegative quadrant; the equal-product relation is a substantive ingredient in (2).

Why maximizer selection satisfies the axioms

The first theorem of Characterization.lean proves each conjunct for an arbitrary maximizer selector $N$. Uniqueness is the common final step.

For Pareto optimality, if $y$ weakly dominates $N(P)$, it is individually rational and its product is at least that of $N(P)$ by monotonicity of multiplication on nonnegative gains.

Thus $y$ is also a maximizer; uniqueness gives $y=N(P)$. This argument checks domination by all feasible points, not merely by an externally restricted Pareto frontier.

On a symmetric problem, swapping $N(P)$ preserves feasibility, individual rationality, and the product. Swapping every comparison point shows that the swapped point is again a maximizer. Uniqueness then forces the two coordinates of $N(P)$ to coincide.

For a positive affine map $A$, direct expansion gives

The positive factor preserves the ordering of products, and positive scales preserve the individual-rationality inequalities. Every point of $A(S)$ has a preimage in $S$, so $A(N(P))$ is a maximizer for the transformed problem. Uniqueness identifies it with $N(Q)$.

Finally, in the IIA situation, $N(Q)\in S$ and disagreement is unchanged. Its larger-set maximality restricts to every individually rational point in $S$, making it a maximizer for $P$. Uniqueness again proves the required equality. Neither this argument nor the axiom grants a contraction that loses the selected point.

The converse via normalization and a bounded enlargement

We now explain the second theorem of Characterization.lean. Let $F$ satisfy the four axioms, and fix a maximizer $x$ for $P=(S,d)$. The positivity argument above yields $x_{i}-d_{i}>0$. Define

This positive affine map sends $d$ to $(0,0)$ and $x$ to $(1,1)$. It preserves compactness and convexity, and the transformed problem $Q=(U,(0,0))$ remains admissible. By (3), $(1,1)$ is a Nash maximizer of $Q$.

A tangent bound for every feasible point

Lemma 7.1. Every $z\in U$ satisfies $z_{1}+z_{2}\le2$.

Proof. Assume $c=z_{1}+z_{2}-2>0$. Set

and choose the explicit positive number

The point $w=(1-t)(1,1)+tz$ belongs to $U$ by convexity. The bounds $tK_{i}\le1/2$ show $w_{i}=1+t(z_{i}-1)\ge1/2$, so $w$ is individually rational even if $z$ itself is not. Expanding the product,

Since $tK\le c/2$, the right side is at least $tc/2>0$. This contradicts maximality of $(1,1)$ on the individually rational part of $U$. $\square$

The source uses nested binary minima to realize (5). This quantitative argument proves a supporting-line inequality for all of $U$. It is important not to infer the inequality directly from $z_{1}z_{2}\le1$: that comparison is available only for individually rational $z$, and even there requires convexity near $(1,1)$ to obtain the linear bound. The proof avoids a differentiability premise.

Constructing an admissible symmetric comparison problem

The half-space $H=\{u:u_{1}+u_{2}\le2\}$ contains $U$, but is not compact and is therefore not itself an admissible bargaining set. The source repairs this by a bounded enlargement. The compact set

has upper and lower bounds for both coordinate projections. From any such bounds $M_{1},m_{1},M_{2},m_{2}$, set

The bounds imply $V\subseteq[-B,B]^{2}$, while Lemma 7.1 and its swapped version give $V\subseteq H$. Consequently $U\subseteq W$.

The set $W$ is compact, convex, and invariant under swapping. It contains both $(0,0)$ and $(1,1)$, so $R=(W,(0,0))$ is an admissible problem. Symmetry gives $F(R)=(r,r)$. Feasibility gives $2r\le2$. If $r<1$, the point $(1,1)\in W$ would dominate $F(R)$ and Pareto optimality would force equality, a contradiction. Thus $r=1$ and

Because $U\subseteq W$ and $(1,1)\in U$, IIA gives $F(Q)=F(R)=(1,1)$. Positive affine invariance then yields $\phi(F(P))=F(Q)=\phi(x)$. The positive scales make $\phi$ injective, so $F(P)=x$, completing the converse.

This use of a symmetric box intersected with a half-space is the actual formal construction. The proof does not require a compact convex hull of $U\cup\operatorname{swap}(U)$, nor an application of the axioms to an unbounded half-space. It also explains why individual rationality need not be postulated for $F$: the axioms determine its output through the comparison problem.

Source organization and verification evidence

The implementation is small enough to inspect by module. Definitions and axiom predicates are in NashBargaining/Basic.lean; attainment is in Existence.lean; midpoint uniqueness is in Uniqueness.lean; both axiom directions are in Characterization.lean; and the four registered wrappers are in Solution.lean. The proof bodies use Mathlib’s topology and convexity interfaces together with real-arithmetic tactics, including ring, linarith, nlinarith, positivity, and field_simp.

Challenge.lean repeats the public definitions and the four target theorem statements, with four deliberate sorry holes. It is the statement-side challenge, not the implementation proof. The comparator configuration maps those declarations to Solution.lean. The inspected implementation files contain no sorry or admit proof placeholders; this textual observation is distinct from a kernel check of their complete dependency closure.

The immutable Palomar record reports the following historical evidence [3]:

• Lean toolchain leanprover/lean4:v4.35.0-rc2 and Mathlib revision 065356127b1dc0016f66b7283ce0ce2c4055aa55;

• verification on September 24, 2026, at 20:19:45 UTC, with workflow run 36053394619;

• permitted axioms propext, Quot.sound, and Classical.choice, with external checker entries for nanoda and con-ron;

• registration on September 25, 2026, and preserved source at the commit identified in Section 1.

The record also reports a neutral editorial outcome with no warnings. That status is not a claim of journal peer review or an endorsement by Nash’s original publisher.

Preparation of this manuscript involved retrieving and inspecting the pinned definitions, proof files, comparator configuration, and dependency metadata, and checking the statement-side and solution-side file hashes against the registry record. We did not perform a fresh Lean build or rerun the registry’s external checkers for this manuscript. The verification claim therefore rests on the dated registry evidence, while the present explanation rests on source inspection. Mathematical validity is relative to the encoded hypotheses and Lean’s foundational assumptions; neither compilation nor registration certifies a broader economic interpretation.

Authorship disclosure and limitations

The manuscript was primarily drafted with GPT 6.1 under the authors’ direction. The submitting author reports understanding some parts of the work; this disclosure does not claim a complete independent human reconstruction or line-by-line human validation of every formal proof. The pinned formalization.yaml separately records AI-assisted proof engineering using gpt-6-luna (Codex CLI). These are distinct disclosures: the manuscript-drafting model is not inferred to be the historical proof-engineering model, and model identity is not verification evidence.

The manuscript and its source are licensed CC BY 4.0. The referenced Lean repository declares BSD-3-Clause; the manuscript license does not relicense that code. The registry lists Arthur Freitas Ramos as the formalization’s author and responsible maintainer. The present manuscript’s three-author byline should not be read as an altered registry attribution or as a statement of undocumented individual contributions.

The development covers neither degenerate problems lacking strictly positive mutual gains nor bargaining among more than two players. It establishes no convergence rates, numerical method, equilibrium implementation, or empirical fairness claim. Its mathematical value is the explicit, source-traceable verification of the classical characterization within the stated compact convex two-person model.