Algorithmic Game Theory

Motivation

A correlated equilibrium (Aumann 1974) describes play in a game where a mediator draws a profile of recommended actions from a joint distribution and tells each player only that player's own recommendation; the distribution is an equilibrium when no player gains, on average, by departing from the recommendation. Correlated equilibria are the natural outcome of regret-minimizing learning dynamics and the solution concept underlying much of algorithmic game theory, so it matters in which games they are guaranteed to exist.

For finite games existence follows from Nash's theorem, since every Nash equilibrium is a correlated one. Hart and Schmeidler (1989) gave a direct proof based on linear duality, with no fixed-point theorem, and then extended it beyond finite games. This mission formalizes the last and most general of their three existence theorems: games with arbitrarily many players whose strategy spaces are compact Hausdorff spaces.

Timeline.

• 1952: Fan and Glicksberg prove fixed-point theorems that yield Nash equilibria, hence correlated equilibria, for continuous games on compact strategy spaces.
• 1969: Peleg proves existence of Nash equilibria for games with infinitely many players, finite strategy sets and continuous payoffs.
• 1974: Aumann introduces correlated equilibria (J. Math. Econ. 1).
• 1987: Aumann characterizes correlated equilibrium as Bayesian rationality (Econometrica 55).
• 1989: Hart and Schmeidler prove existence of correlated equilibria by a separation argument: Theorem 1 for finite games, Theorem 2 for infinitely many players with finite strategy sets, Theorem 3 for compact Hausdorff strategy spaces (Math. Oper. Res. 14).

Setting

A game consists of a nonempty set $N$ of players, possibly uncountable; for each player $i\in N$ a nonempty set $S^i$ of pure strategies; and for each player a payoff function $h^i:S\to\mathbb R$ on the set of strategy profiles $S=\prod_{j\in N}S^j$. For a profile $s$ and a strategy $t^i\in S^i$, $(s^{-i},t^i)$ denotes the profile obtained from $s$ by replacing player $i$'s coordinate with $t^i$; thus $h^i(s)=h^i(s^{-i},s^i)$.

In this mission each $S^i$ is a compact Hausdorff space with its Borel σ-algebra $\Sigma^i$, the profile space $S$ carries the product topology, and $\Sigma$ is the Borel σ-algebra of $S$. The product σ-algebra $\Sigma_0$ generated by the $\Sigma^i$ is contained in $\Sigma$, and the inclusion may be strict when $S$ is not metrizable (the paper's footnote 13).

Let $p$ be a probability measure on $(S,\Sigma)$. Think of $p$ as the mediator's distribution; player $i$ learns the coordinate $s^i$ of the drawn profile. A deviation of player $i$ is a $\Sigma^i$-measurable map $\zeta^i:S^i\to S^i$ that replaces each recommendation by an action. The measure $p$ is a correlated equilibrium with respect to $\{\Sigma^i\}_{i\in N}$ and $\Sigma$ when, for every player $i$ and every deviation $\zeta^i$,

$$\int_S\bigl[h^i(s^{-i},s^i)-h^i\bigl(s^{-i},\zeta^i(s^i)\bigr)\bigr]\,dp(s)\ \ge\ 0 . \tag{4}$$

The left side is the expected gain from obeying the recommendation instead of following $\zeta^i$.

Formalization targets

Goal: Theorem 3

If every $S^i$ is compact Hausdorff and every $h^i$ is continuous on $S$ with the product topology, then

$$\exists\, p\ \text{probability measure on } (S,\Sigma)\ \text{such that (4) holds for all } i\in N \text{ and all } \Sigma^i\text{-measurable } \zeta^i .$$

"Countably additive" in the paper's statement is automatic: $p$ is a measure.

Milestones, in the order of the proof

1. Every f-set game has a correlated equilibrium. An f-set is a product $T=\prod_iT^i$ of finite nonempty sets $T^i\subseteq S^i$ with $T^i$ a singleton for all but finitely many $i$; the game $\Gamma_T$ restricts each player to $T^i$, and its correlated equilibrium $q_T$ is a finitely supported probability on $S$.
2. On a compact Hausdorff space, every net of probability measures has a regular probability measure as a cluster point for the topology induced by the continuous functions.
3. For a regular probability $p$ on $S$ and a Borel set $R^i\subseteq S^i$, there are a closed $F^i\subseteq R^i$ and an open $G^i\supseteq R^i$ with $p\bigl((G^i\setminus F^i)\times S^{-i}\bigr)<\varepsilon$: the marginal of a regular measure is regular.
4. The special case. A regular cluster point $p$ of the $q_T$ satisfies (4) for every deviation that equals a fixed $t^i$ on a Borel set $R^i$ and the identity elsewhere.
5. For continuous $h^i$ and $\varepsilon>0$, $S^i$ has a finite Borel partition $A_1,\dots,A_K$ with $|h^i(s^{-i},a)-h^i(s^{-i},b)|<\varepsilon$ for $a,b$ in the same piece and every $s^{-i}$.
6. The general case. If (4) holds for all deviations of the special form, it holds for every Borel deviation.

An optional milestone records the remark on p. 23 that, for a finite strategy set $S^i$, condition (4) for player $i$ is equivalent to the earlier condition (3), one inequality per recommendation $r^i$ and alternative $t^i$.

Significance

The result. Theorem 3 guarantees correlated equilibria, with a genuine (countably additive) probability measure, in every continuous game on compact strategy spaces, however many players there are. It also justifies taking $\Sigma$ to be the full Borel σ-algebra rather than the smaller product σ-algebra, so that every Borel-measurable deviation rule is allowed. Nash existence under the same hypotheses (Fan 1952, Glicksberg 1952) implies existence of correlated equilibria too, but through a fixed-point theorem; the proof here uses only finite-dimensional duality and compactness.

Formalizing it. The theorem is classical and its proof is published; nothing here is open. To our knowledge no machine-checked proof of Theorem 3, or of any existence result for correlated equilibria in infinite games, exists. Finite-game existence results are on the platform (AGT.nash_existence; the correlated-equilibrium encodings of Aumann 1987 and Foster and Vohra 1997, and AGT.swap_regret_correlated_equilibrium). The formalization would add reusable measure-theoretic tools on compact products: the regular cluster point of a net of probability measures, the regularity of marginals, and uniform partitions for continuous functions on a product.

Difficulty

The obvious argument is the one that proves Theorem 2: approximate the game by finite games $\Gamma_T$, take correlated equilibria $q_T$, extract a weak-* cluster point $p$, and pass the inequalities of $\Gamma_T$ to the limit. Passing to the limit works only for integrands that are continuous in $s$, because $p$ is a cluster point against continuous functions only. The integrand of (4) is $h^i(s)-h^i(s^{-i},\zeta^i(s^i))$, and $\zeta^i$ is merely Borel measurable, so this integrand need not be continuous and the limit step fails. Restricting to continuous deviations would avoid the difficulty but would prove a weaker theorem. Two further points need care: on a non-metrizable product the Borel σ-algebra is larger than the product σ-algebra, and the f-sets ordered by inclusion are not a directed set.

Formalization scope

The profile space is a type synonym Profile S of ∀ i, S i carrying the product topology and the instance borel (Profile S), so measures on $S$ live on the Borel σ-algebra $\Sigma$ and not on Mathlib's product σ-algebra MeasurableSpace.pi ($=\Sigma_0$). The pair $(s^{-i},t^i)$ is Function.update s i t. Players form a type ι with Nonempty ι; each S i is nonempty, compact and Hausdorff with BorelSpace (S i); payoffs are h : ι → Profile S → ℝ with each h i continuous. Deviations are all maps ζ : S i → S i with Measurable ζ.

The predicate IsCorrelatedEq h μ requires IsProbabilityMeasure μ and, for each player and measurable deviation, both integrability of the integrand and nonnegativity of its integral. The integrability clause prevents a trivializing reading in which a non-integrable integrand, whose Lean integral is $0$, satisfies (4) vacuously; restricting deviations to continuous maps, or using the product σ-algebra, would also change the theorem and is ruled out.

The f-set net is indexed by the f-sets containing a fixed profile $\hat s$, which are directed; the paper's "ordered by inclusion of the sets $T$" over all f-sets is not directed, and anchoring repairs this without affecting any statement of the paper. A correlated equilibrium $q_T$ of $\Gamma_T$ is encoded by its finite support and weights (IsFSetCE). The special case is stated for a regular cluster point of the $q_T$ given by these constructed objects, not for an arbitrary measure.

A complete development needs Banach–Alaoglu or the compactness of probability measures on a compact space, the Riesz–Markov–Kakutani representation (RealRMK), regularity of measures (Measure.Regular), Urysohn's lemma, and uniform continuity on compact spaces, all available in Mathlib in some form. Proofs of any milestone, including the general-purpose milestones 2, 3 and 5, are welcome.

Selected references

• S. Hart and D. Schmeidler, Existence of Correlated Equilibria, Mathematics of Operations Research 14(1), 18–25, 1989. https://doi.org/10.1287/moor.14.1.18
• R. J. Aumann, Subjectivity and Correlation in Randomized Strategies, Journal of Mathematical Economics 1, 67–96, 1974. https://doi.org/10.1016/0304-4068(74)90037-8
• R. J. Aumann, Correlated Equilibrium as an Expression of Bayesian Rationality, Econometrica 55(1), 1–18, 1987. https://doi.org/10.2307/1911154
• B. Peleg, Equilibrium Points for Games with Infinitely Many Players, Journal of the London Mathematical Society s1-44, 292–294, 1969. https://doi.org/10.1112/jlms/s1-44.1.292
• I. L. Glicksberg, A Further Generalization of the Kakutani Fixed Point Theorem, with Application to Nash Equilibrium Points, Proceedings of the AMS 3, 170–174, 1952. https://doi.org/10.1090/S0002-9939-1952-0046638-5
• K. Fan, Fixed-Point and Minimax Theorems in Locally Convex Topological Linear Spaces, PNAS 38, 121–126, 1952. https://doi.org/10.1073/pnas.38.2.121
• N. Dunford and J. T. Schwartz, Linear Operators, Part I, Interscience, 1958.

Motivation

Two parties who can cooperate for mutual benefit must still agree on how to share the benefit. In The Bargaining Problem (Econometrica, 1950) John Nash asked which agreement two rational bargainers of equal skill should reach. His answer is not a model of haggling: it is a list of conditions any reasonable rule should satisfy, together with a proof that exactly one point of the set of feasible agreements is compatible with them. That point maximizes the product of the two parties' utility gains. Known as the Nash bargaining solution, it is the reference point of cooperative bargaining theory. Economics, operations research and networking all use it: in supply contracts, in wage bargaining, and in fair bandwidth allocation, where maximizing a product of gains becomes maximizing a sum of logarithms (proportional fairness).

Timeline:

• 1944. von Neumann and Morgenstern axiomatize expected utility. A utility is determined up to a positive affine transformation $au+b$. Nash quotes this on p. 157.
• 1950. Nash introduces the two-person bargaining problem and the axioms of Pareto efficiency, independence of irrelevant alternatives and symmetry, the solution being invariant under the choice of utility scales. He proves that they force the maximizer of the product $u_1u_2$ (doi:10.2307/1907266).
• 1953. Nash's Two-Person Cooperative Games adds the threat game that fixes the disagreement point.
• 1975. Kalai and Smorodinsky replace independence of irrelevant alternatives by monotonicity and obtain a different solution.
• 1986. Binmore, Rubinstein and Wolinsky show that the Nash solution is the limit of equilibria of alternating-offers bargaining as the time between offers vanishes.

Setting

A bargaining problem is a pair $\langle S,d\rangle$. Here $S\subseteq\mathbb R^2$ is the set of utility pairs $u=(u_1,u_2)$ the two players can reach by agreement, including lotteries over agreements. $d\in S$ is the disagreement point, the utilities of no cooperation. As in the platform goal, $S$ is compact and convex, and some $s\in S$ has $s_1>d_1$ and $s_2>d_2$ (both individuals could gain). Write $\mathcal B$ for the set of such pairs.

A bargaining solution is a map $g$ from $\mathcal B$ to $\mathbb R^2$. Nash requires:

• Selection. $g(S,d)\in S$.
• PAR (Nash's assumption 6). If $s,t\in S$ and $t$ is strictly better than $s$ for both players, then $g(S,d)\neq s$.
• IIA (assumption 7). If $S\subseteq T$ and $g(T,d)\in S$, then $g(S,d)=g(T,d)$.
• SYM (assumption 8). If $d_1=d_2$ and $S$ is symmetric in the line $u_1=u_2$, then $g(S,d)$ lies on that line.
• INV. For $L(s)=(\alpha_1s_1+\beta_1,\ \alpha_2s_2+\beta_2)$ with $\alpha_1,\alpha_2>0$, $g(L(S),L(d))=L(g(S,d))$.

The paper has no separate INV axiom. It normalizes the disagreement utility to $0$ and notes that each utility is then determined only up to a positive multiple (p. 158), so the solution must not depend on that choice.

Formalization targets

Goal

The goal is the platform theorem NashBargaining.nash_bargaining_solution_unique, posed by Nickrobbins95 and currently Open. This mission references it and does not restate it. It asserts that there is a solution $f$ such that a solution $g$ satisfies selection, INV, SYM, IIA and PAR if and only if $g=f$, and that for every $\langle S,d\rangle\in\mathcal B$

$$f(S,d)\ge d,\qquad (s_1-d_1)(s_2-d_2)<(f_1-d_1)(f_2-d_2)\ \text{ for all } s\in S,\ s\ge d,\ s\neq f(S,d).$$

Nash's paper proves the necessity half: a solution satisfying the conditions must select the maximizer of the Nash product. The sufficiency half, that the maximizer map satisfies the five conditions, is not argued in the paper. It must be supplied by whoever closes the goal.

Milestones

1. On a compact convex $S\ni(0,0)$ that contains a point where both players gain, $u_1u_2$ has exactly one strict maximizer $p$ in the closed first quadrant, and $p_1,p_2>0$.
2. Multiplying the utilities by positive constants maps the maximizer to the maximizer, so $p$ may be moved to $(1,1)$.
3. If $S$ is convex and $(1,1)$ maximizes $u_1u_2$, then $u_1+u_2\le2$ on all of $S$.
4. A compact $S$ under that line lies in a square $Q_h=\{2-2h\le u_1+u_2\le2,\ |u_1-u_2|\le h\}$.
5. $(1,1)$ is the only point of $Q_h$ on the diagonal that no point of $Q_h$ strictly dominates.
6. Necessity. Under the five conditions, $g(S,d)$ is the strict maximizer of $(s_1-d_1)(s_2-d_2)$ over $S\cap\{s\ge d\}$.

Two further items formalize the paper's examples: the Bill–Jack barter, whose solution is the vertex $(12,5)$ reached by exactly one exchange, and trade with money, where the solution gives equal money profits.

Significance

The Nash product characterization is used, mostly without proof, wherever a "fair" split of a cooperative surplus is needed. Examples are generalized Nash bargaining in supply-chain contracting and labour economics, the proportional-fairness criterion in network rate control, and the Nash-in-Nash models of bilateral negotiations. Many papers that build on it apply it to a specific feasible set. They therefore rely on the necessity direction, which is the step that makes the maximizer the unique answer rather than one answer among several.

The result has been proved since 1950, while the referenced Prove2Me goal remains Open. This mission supplies the milestones of Nash's own argument in the encoding of that goal, so that the necessity direction can be assembled from them. Sufficiency remains as separate work. The two examples are small, concrete checks of the solution concept.

Difficulty

Each step is elementary. The difficulty is in keeping the bookkeeping honest across the normalizations. The axioms are stated on the class $\mathcal B$, and a solution is a function on a subtype. Every application of INV, SYM or IIA therefore needs a membership proof for a transformed set: the image of $S$ under an affine map, or the enclosing square. It also needs the disagreement point to be carried along. The tempting short cut is to argue "without loss of generality $d=0$ and $p=(1,1)$". That is exactly what INV licenses, but only after compactness, convexity, the point where both gain, and the location of $d$ inside the square have been re-established for each transformed problem. Uniqueness of the maximizer also needs care at the boundary of the quadrant, where the product vanishes.

Formalization scope

Utility pairs are ℝ × ℝ, with u.1 player 1's utility and u.2 player 2's. Milestones 1–5 work at $d=(0,0)$, the paper's normalization. Milestone 6 has a general $d$ and the goal's encoding. Milestones 1–5 make the following readings explicit:

• "First quadrant" is the closed quadrant $u_1\ge0,\ u_2\ge0$.
• "The point where $u_1u_2$ is maximized" is the strict maximizer over $S$ in that quadrant, in the goal's form. Milestone 1 also states $p_1,p_2>0$, which follows from the point where both gain (p. 158).
• Milestone 3's hypothesis is the weak maximum $s_1s_2\le1$. Its conclusion covers every point of $S$, not only first-quadrant points.
• The square is the explicit set $Q_h$. Its compactness, convexity and literal symmetry $(a,b)\in Q_h\iff(b,a)\in Q_h$ are part of milestone 4's conclusion.
• "Satisfying assumptions (6) and (8)" in the square means lying on $u_1=u_2$ and being strictly dominated by no point of the square.

Milestone 6's five hypotheses are copied verbatim from the goal, and its conclusion is the goal's last conjunct for the given $g$. It does not restate the goal: it has no existence claim and no "if and only if".

Trivializing formalizations are ruled out. The point where both gain is a hypothesis wherever uniqueness is claimed; without it a segment on an axis has many maximizers of $u_1u_2=0$. The square is a concrete set, not "some symmetric compact convex set", and the solution's properties are quantified over the goal's class $\mathcal B$, which is nonempty.

The examples need finite sums, convex hulls of finite sets, and extreme points, all in Mathlib. Contributions are welcome on each milestone and on the sufficiency half of the goal.

Related platform work treats other bargaining models. These are Rubinstein's alternating-offers game (RubinsteinBargaining.PEP) and the Chatterjee–Samuelson sealed-offer double auction (ChatterjeeSamuelson). Neither is used here. The von Neumann–Morgenstern utility theorem behind the normalization is formalized as TheoryOfGames.Utility.utility_existence_uniqueness.

Selected references

• J. F. Nash, Jr., The Bargaining Problem, Econometrica 18(2), 155–162, 1950. doi:10.2307/1907266
• J. von Neumann, O. Morgenstern, Theory of Games and Economic Behavior, Princeton University Press, 1944.
• J. F. Nash, Jr., Two-Person Cooperative Games, Econometrica 21(1), 128–140, 1953. doi:10.2307/1906951
• E. Kalai, M. Smorodinsky, Other Solutions to Nash's Bargaining Problem, Econometrica 43(3), 513–518, 1975. doi:10.2307/1914280
• K. Binmore, A. Rubinstein, A. Wolinsky, The Nash Bargaining Solution in Economic Modelling, RAND Journal of Economics 17(2), 176–188, 1986. doi:10.2307/2555382
• M. J. Osborne, A. Rubinstein, Bargaining and Markets, Academic Press, 1990, Theorem 2.3.

Motivation

A supplier that sells through independent retailers usually loses part of the profit an integrated firm would earn: each retailer orders to maximize its own profit, not the channel's. Supply chain coordination asks which contracts make the decentralized choices coincide with the integrated optimum. Cachon and Lariviere study revenue-sharing contracts, under which a retailer pays a per-unit wholesale price and keeps only a fraction $\phi$ of its revenue, the rest going to the supplier. The contracts were made prominent by the video rental industry around 1998, where studios lowered tape prices in exchange for a share of rental income.

With a single retailer, revenue sharing at the wholesale price $\phi c$ coordinates the channel and splits its profit in the proportion $\phi$. This mission formalizes the extension in Section 3.2 of the paper to competing retailers: several locations whose revenues depend on each other's stock, so that one retailer's order lowers the others' revenue. Competition creates externalities the single-retailer argument does not have, and the question is whether revenue sharing still coordinates, and at what prices. Section 4.1.2 then works out a Cournot example in closed form, measuring how far the supplier's own optimal wholesale price leaves the channel from the integrated profit.

The source is the authors' working paper of June 2000; the published version (Management Science 51(1), 2005) renumbers and revises the results. The working paper numbers no theorem, so results are cited by section, displayed equation and page.

Setting

A single supplier sells one product through $n$ locations $i = 1,\dots,n$, each run by an independent retailer. A stocking profile is $\bar q = (q_1,\dots,q_n)$, and the revenue at location $i$ is $R_i(\bar q)$, which may depend on every location's quantity. The system revenue is $R(\bar q) = \sum_i R_i(\bar q)$, every unit costs the supplier $c > 0$, and the integrated system profit is

$$\Pi(\bar q) = R(\bar q) - c\sum_{i=1}^n q_i .$$

Write $R_j^i(\bar q) = \partial R_j(\bar q)/\partial q_i$: the superscript is the variable differentiated, the subscript the revenue function. The paper assumes that each $R_i$ is continuous, that $\partial^2 R_i/\partial q_i\partial q_j \le 0$ for $j \ne i$ (locations are substitutes), and that $R_i$ is unimodal in $q_i$. The system-optimal profile $\bar q^I$ has positive entries and solves the first-order system

$$R_i^i(\bar q^I) + \sum_{j\ne i} R_j^i(\bar q^I) = c, \qquad i = 1,\dots,n. \tag{6}$$

Under a revenue-sharing contract $(\phi, w_i)$ retailer $i$ earns $\pi_{r_i}(\bar q,\phi,\bar w) = \phi R_i(\bar q) - w_i q_i$ and the supplier earns $\pi_s(\bar q,\phi,\bar w) = \sum_i\big((1-\phi)R_i(\bar q) + w_i q_i\big) - c\sum_i q_i$; the wholesale-price contract is $\phi = 1$, with profits written $\pi_{r_i}(\bar q,\bar w)$ and $\pi_s(\bar q,\bar w)$. A Nash equilibrium in order quantities is a profile $\bar q \ge 0$ from which no retailer gains by changing its own quantity to any $x \ge 0$. The coordinating wholesale prices are

$$w_i^I = c - \sum_{j\ne i} R_j^i(\bar q^I).$$

The Cournot example (7) is $R_i(\bar q) = q_i\big(1 - q_i - \beta\sum_{j\ne i} q_j\big)$ with $0 \le \beta < 1$.

Formalization targets

Goal: revenue sharing supports $\bar q^I$ (Sec. 3.2, p. 14)

For $\phi\in[0,1]$ and $w_i(\phi) = \phi w_i^I$:

$$\bar q^I \text{ is a Nash equilibrium},\quad \pi_{r_i}(\bar q^I,\phi,\phi\bar w^I) = \phi\,\pi_{r_i}(\bar q^I,\bar w^I),\quad \pi_s(\bar q^I,\phi,\phi\bar w^I) = (1-\phi)\Pi(\bar q^I) + \phi\,\pi_s(\bar q^I,\bar w^I).$$

Wholesale-price contracts (Sec. 3.2, pp. 13–14)

An interior equilibrium satisfies $R_i^i(\bar q^N) = w_i$ (Eq. (8)), so marginal-cost pricing does not support $\bar q^I$ when a location imposes a negative externality; the prices $\bar w^I$ make $\bar q^I$ an equilibrium; $w_i^I \ge c$ when cross-effects are nonpositive; and $\bar w^I$ supports exactly the split $\pi_s(\bar q^I,\bar w^I) = \sum_i q_i^I\sum_{j\ne i}(-R_j^i(\bar q^I))$.

Revenue sharing (Sec. 3.2, p. 14)

An interior equilibrium satisfies $\phi R_i^i(\bar q^N) = w_i(\phi)$; the two profit identities hold for every $\phi$; and $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$.

The Cournot example (Sec. 4.1.2, pp. 19–20)

At a common price $w<1$ the unique equilibrium is $q_i^N = (1-w)/(2+\beta(n-1))$; the integrated optimum is $q_i^I = (1-c)/(2+2\beta(n-1))$; the coordinating price $w^I = c + \beta(n-1)(1-c)/(2+2\beta(n-1))$ increases in $\beta$ and $n$; the supplier's optimal price is $w^* = (1+c)/2$; and the efficiency at $w^*$ is

$$\frac{\Pi(\bar q^N(w^*))}{\Pi(\bar q^I)} = 1 - \frac{1}{(2+\beta(n-1))^2}.$$

Significance

The goal shows that the single-retailer coordination result survives competition, with one change: the coordinating price must charge each retailer for the externality it imposes on the others, so it depends on every location's revenue function, and $w^I_i$ exceeds the production cost. The supplier's profit then moves along a line between what wholesale prices alone give her and the whole system profit, which is how revenue sharing provides a profit split that linear prices cannot. The Cournot results make the comparison quantitative: when retailers compete intensely, the supplier's own optimal wholesale price already achieves most of the integrated profit, so revenue sharing, which has administrative costs, is less attractive.

No machine-checked proof of these results is known. The mission produces a reusable formal description of an $n$-player quantity game under per-retailer linear contracts, equilibrium conditions for it, and a fully worked Cournot instance, including a uniqueness claim for equilibria among all (not only symmetric) profiles.

Difficulty

The equilibrium claims are global: a retailer must not gain from any nonnegative deviation, not only from small ones. A first-order condition at $\bar q^I$ does not give this by itself. The page assumes $R_i$ unimodal in $q_i$, but unimodality does not survive subtracting the linear purchase cost, so the first-order condition is not sufficient under that assumption alone; the formalization uses concavity in the own quantity, under which it is. The participation claim $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ is stated on the page without proof and needs a bound on the revenue of a location that stocks nothing.

In the Cournot example, uniqueness of the equilibrium must exclude asymmetric profiles and profiles where some retailers stock nothing, and the supplier's optimal price must be compared against every equilibrium at every price, including prices at which the retailers order nothing.

Formalization scope

Locations are Fin n; a profile is Fin n → ℝ; revenues are R : Fin n → (Fin n → ℝ) → ℝ, and dR i j q is $R_j^i(\bar q) = \partial R_j/\partial q_i$, given as a partial derivative at every profile with all entries positive. A deviation of retailer $i$ to $x$ is Function.update q i x, and Nash equilibria quantify over all $x \ge 0$. The standing assumptions of Section 3.2 are fields of the structure Model: $c > 0$; continuity of $R_i$ on the nonnegative orthant; the partial derivatives; $\partial^2 R_i/\partial q_i\partial q_j \le 0$, encoded as "$R_i^i$ does not increase in $q_j$"; and concavity of $R_i$ in $q_i$, which is the formalization's reading of "unimodal in $q_i$". The paper's assumption that marginal revenue eventually falls below every $\delta > 0$ is used only for existence of an equilibrium, which is not formalized, and is omitted.

Deviations from the page, each disclosed in the item concerned:

• $\bar q^I$ is taken as any positive solution of (6); its optimality for $\Pi$ is not used.
• "$\bar q^*$ is a Nash equilibrium" (p. 13) is read as $\bar q^I$.
• In $\phi(R_i(\bar q^I) - q_i^I w_i)$ (p. 14), $w_i$ is read as $w_i^I$.
• "$R_i^i(\bar q^I) > c$" needs a negative externality $\sum_{j\ne i}R_j^i(\bar q^I) < 0$, which is assumed.
• "$R_j^i(\bar q) \le 0$" is not a standing assumption, so it is a hypothesis of $w_i^I \ge c$, and strictness needs some strictly negative cross-effect.
• $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ assumes nonnegative revenue at a location that stocks nothing.
• In the Cournot example the implicit $w < 1$ and $0 < c < 1$ are hypotheses; all retailers pay a common price; "increasing" is strict exactly where it holds ($n \ge 2$ for $\beta$, $\beta > 0$ for $n$).

A formalization that defines "the prices coordinate" as "the prices satisfy the first-order condition at $\bar q^I$" restates (6) and is ruled out: every equilibrium claim here is the game-theoretic statement about unilateral deviations. Contributions welcome: proofs of the equilibrium lemmas from concavity and the derivative, the Cournot uniqueness argument, and a general existence theorem for the quantity game.

Selected references

• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991 (Theorem 1.2, existence of pure-strategy equilibria).
• F. Bernstein, A. Federgruen, Pricing and Replenishment Strategies in a Distribution System with Competing Retailers, Operations Research 51(3):409–426, 2003. https://doi.org/10.1287/opre.51.3.409.14957
• J. Tirole, The Theory of Industrial Organization, MIT Press, 1988.

Motivation

Many networks are built and paid for by the users they serve: multicast trees, virtual overlays, shared subnetworks of the Internet. A protocol proposes a design and a rule for splitting its cost, and each participant is free to accept the proposal or defect to a cheaper alternative. The designer therefore cannot impose the global optimum; the best it can do is propose the cheapest outcome that no participant wants to leave, a Nash equilibrium. The ratio between the cost of the best equilibrium and the optimal cost, the price of stability, measures the loss caused by requiring stability. It contrasts with the price of anarchy, which compares the worst equilibrium with the optimum and suits settings with no coordinating protocol at all.

Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008; preliminary version FOCS 2004) studied this question for the most common cost-sharing rule, the Shapley (equal-split) rule, under which every user of an edge pays the same share of its cost. Their first result, the subject of this mission, is that the price of stability is at most the harmonic number $H(k)$, where $k$ is the number of players, and that this bound is attained in the limit.

Setting

There are $k$ players and a finite set $E$ of edges. Each player $i$ has a family $\Sigma_i$ of feasible strategies, each a set of edges; in the network setting $\Sigma_i$ consists of the edge sets connecting player $i$'s terminals in a directed graph. Each edge $e$ has a nonnegative cost $c_e$. In a strategy vector $S=(S_1,\dots,S_k)$, $S_i\in\Sigma_i$, let $x_e$ be the number of players whose strategy contains $e$. Under Shapley cost sharing player $i$ pays

$$C_i(S)=\sum_{e\in S_i}\frac{c_e}{x_e}.$$

The cost of the designed network is

$$\operatorname{cost}(S)=\sum_{e\in\bigcup_i S_i}c_e ,$$

and the payments add up to exactly this amount. The profile $S$ is a (pure) Nash equilibrium if no player $i$ has a strategy $S_i'\in\Sigma_i$ with $C_i(S_{-i},S_i')<C_i(S)$. Finally,

$$H(k)=1+\tfrac12+\dots+\tfrac1k .$$

The game is a congestion game: the per-user cost of an edge, $f_e(x)=c_e/x$, depends only on the edge and its number of users. Rosenthal's potential

$$\Phi(S)=\sum_{e\in E}\sum_{x=1}^{x_e}f_e(x)$$

changes by exactly the deviating player's change in cost when a single player changes strategy. The same objects are used with load-dependent edge costs $c_e(x)$, in which case $f_e(x)=c_e(x)/x$.

Formalization targets

Goal: Theorem 2.1 and its tightness

For every game with $c_e\ge0$ in which each player has a feasible strategy there is a Nash equilibrium $S$ with

$$\operatorname{cost}(S)\le H(k)\cdot\operatorname{cost}(P)\quad\text{for every profile }P,$$

and for every $k\ge1$, $\varepsilon>0$ the instance of Fig. 1.1 (player $i$ has its own path of cost $1/i$, and all players can share a path of cost $1+\varepsilon$) has a Nash equilibrium, every Nash equilibrium of it costs $H(k)$, and some profile costs $1+\varepsilon$. The ratio $H(k)/(1+\varepsilon)$ tends to $H(k)$ as $\varepsilon\to0$.

Milestones

1. Budget balance: $\sum_iC_i(S)=\operatorname{cost}(S)$ for every $S$ (Sect. 1).
2. Rosenthal's potential is exact (Theorem 2.1, proof, (2.1)).
3. From every profile some Nash equilibrium of no larger potential is reached (Theorem 2.1, proof).
4. Theorem 3.1: if $\operatorname{cost}(S)\le A\,\Phi(S)$ and $\Phi(S)\le B\operatorname{cost}(S)$ for all $S$, the price of stability is at most $AB$.
5. For nondecreasing concave edge costs $c_e(x)$: $\operatorname{cost}(S)\le\Phi(S)\le H(k)\operatorname{cost}(S)$ (Theorem 2.3, proof).
6. Theorem 2.3: the $H(k)$ bound for nondecreasing concave edge costs.
7. The Fig. 1.1 instance: its Nash equilibrium is unique and costs $H(k)$; a profile costs $1+\varepsilon$.

Significance

The bound shows that requiring stability under the Shapley rule costs at most a logarithmic factor, $H(k)=\Theta(\log k)$, whereas the price of anarchy of the same game is $k$ (two parallel edges of costs $1$ and $k$ already show this). It was among the first price-of-stability results and is the starting point for a line of work on network design games: the undirected case, where the $H(k)$ bound is not tight and the correct value remained open for years, weighted players, and other cost-sharing rules. The argument (an exact potential that over- and under-estimates the social cost by bounded factors) is the standard tool for price-of-stability bounds, and Theorem 3.1 isolates it in a reusable form.

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal account of Shapley cost-sharing games as congestion games, of Rosenthal's potential and the finite improvement property, of the potential-sandwich argument of Theorem 3.1, and of the matching lower-bound instance, for constant and for nondecreasing concave edge costs.

Difficulty

The obvious approach, bounding the cost of an arbitrary equilibrium, fails: some equilibria cost $k$ times the optimum, so any proof must select a particular equilibrium. The selection uses the finiteness of the strategy space together with the exact potential, and the bound needs the inequality $\Phi\le H(k)\cdot\operatorname{cost}$, which for concave costs requires the per-user cost $c_e(x)/x$ to be nonincreasing. On the lower-bound side, the claim that every equilibrium of Fig. 1.1 costs $H(k)$ requires excluding all equilibria in which some players share the common path, for every $k$ at once, not only checking that the all-own profile is stable.

Formalization scope

Games are encoded as congestion games over arbitrary finite families of edge sets, reusing the published CongestionPoA.AsymSum.Model (congestion game, loads, player costs, cost-form pure Nash equilibrium, total cost). The paper notes that its proofs do not use the graph structure; the directed-graph game is the instance in which $\Sigma_i$ is the family of edge sets connecting player $i$'s terminals. Players and edges form finite types; $k$ is the number of players and $H(k)$ is Mathlib's harmonic k cast to $\mathbb R$. The price of stability is stated as the existence of a Nash equilibrium whose cost is at most the constant times the cost of every profile, with no division by the optimum, and with the hypothesis that some profile exists. Concave costs are functions on $\mathbb N$ with nonincreasing increments, nondecreasing, with $c_e(0)\ge0$; this last condition is implicit in the paper and needed for $c_e(x)/x$ to be nonincreasing. Theorem 3.1 carries the implicit hypothesis $A\ge0$.

A statement that bounds every equilibrium is false, and one that asserts a cheap profile without the Nash condition is trivial; both are excluded, and the tightness part quantifies over every Nash equilibrium of the instance and asserts that one exists.

Needed infrastructure: finite improvement paths in potential games, sum manipulations over loads, and bounds on harmonic sums. The potential lemmas apply to every finite congestion game and are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM J. Comput. 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games Econ. Behav. 14:124–143, 1996. https://doi.org/10.1006/game.1996.0044

Motivation

Nash's theorem guarantees that every finite game has a mixed equilibrium, but says nothing about how hard one is to find. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) showed that computing a Nash equilibrium is complete for the class PPAD of total search problems whose solutions are guaranteed by a parity argument on a directed graph (Papadimitriou 1994). Their proof simulates an arithmetic circuit by a graphical game: a multiplayer game in which each player's payoff depends on a few neighbours only, built from small game gadgets whose equilibria compute $x \mapsto \alpha x$, $x + y$, $xy$, constants and comparisons on mixed-strategy probabilities.

These gadgets are the reusable core of the reduction. The PPAD-completeness results for three-player games, and the later results for two-player games and for approximate equilibria, all rest on gadget analyses of this kind.

Timeline.

• 1994: Papadimitriou defines PPAD and shows that Nash equilibrium computation lies in it (JCSS 48).
• 2001: Kearns, Littman and Singh introduce graphical games (UAI 2001).
• 2005–2006: Goldberg and Papadimitriou reduce $r$-player games to four-player games, and Daskalakis, Goldberg and Papadimitriou prove PPAD-completeness for four players (STOC 2006). The three-player case is obtained independently by Daskalakis and Papadimitriou and by Chen and Deng (ECCC reports, 2005); the two-player case by Chen and Deng (FOCS 2006; J. ACM 56(3), 2009, with Teng).
• 2009: the journal version unifies the three-player argument; its Proposition 4.18 is the gadget $\mathcal G_{+,*}$ that makes the reduction to three players work.

Setting

A game has finitely many players; player $p$ has a finite set $S_p$ of pure strategies and a nonnegative payoff $u^p_s$ for each pure profile $s$. A mixed profile $x$ gives each player a probability distribution $(x^p_j)_{j\in S_p}$, and $x_s$ denotes the product of the probabilities of the components of a partial profile $s$. The expected payoff of a pure strategy $j$ of $p$ is $\sum_{s\in S_{-p}} u^p_{js}x_s$.

An $\epsilon$-Nash equilibrium (the paper's notion, an $\epsilon$-approximately well-supported equilibrium, Eq. (2)) is a mixed profile in which no player puts weight on a pure strategy that another of its pure strategies beats by more than $\epsilon$:

$$\forall p,\ j, j' \in S_p:\quad \sum_{s\in S_{-p}} u^p_{js}x_s > \sum_{s\in S_{-p}} u^p_{j's}x_s + \epsilon \implies x^p_{j'} = 0 .$$

For $\epsilon = 0$ this characterizes Nash equilibria.

A player with strategies $\{0,1\}$ is binary; $\mathbf p[v]$ is the probability that it plays $1$, and $\mathbf p[v : s]$ is the probability that $v$ plays $s$. The affects graph (Definition 2.2) has an edge $(v_1, v_2)$ between distinct players when the payoff of $v_2$ is a nonconstant function of the action of $v_1$. A legal $k$-coloring (Definition 4.8) gives each player one of $k$ colors so that the two ends of an edge differ and two distinct players with a common successor differ.

The game $\mathcal G_{+,*}$ (Fig. 11) has inputs $v_1, v_2$, output $v_3$ and intermediate players $w_1, v_1', w_2, v_2', w_3, w, u$, all binary except $v_2'$, which has strategies $\{0, 1, *\}$. Its payoff tables are fixed by nonnegative integers $\alpha, \beta, \gamma$; the inputs' payoffs are unconstrained.

Formalization targets

Goal: Proposition 4.18

For nonnegative integers $\alpha, \beta, \gamma$ with $\alpha + \beta + \gamma \le 3$, the affects graph of $\mathcal G_{+,*}$ has a legal 3-coloring, and for every $\epsilon \in [0, 0.01]$, at every $\epsilon$-Nash equilibrium,

$$\Big|\,\mathbf p[v_3] - \min\{1,\ \alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2]\}\Big| \le 81\,\epsilon .$$

The case $\epsilon = 0$ is exact computation at every Nash equilibrium.

Milestones: the four claims of the proof

• Claim 1: $\mathbf p[v_1'] = \tfrac18\mathbf p[v_1] \pm \epsilon$.
• Claim 2: $\mathbf p[v_2' : 1] = \tfrac18\mathbf p[v_2] \pm \epsilon$.
• Claim 3: $\mathbf p[v_2' : *] = \tfrac{\alpha}{8}\mathbf p[v_1] + \tfrac{\beta}{8}\mathbf p[v_2] + \tfrac{\gamma}{8}\mathbf p[v_1]\mathbf p[v_2] \pm 10\epsilon$.
• Claim 4: the output bound of the goal.

Milestones: the elementary gadgets

• Proposition 4.2 ($\mathcal G_{\times\alpha}$): $\mathbf p[v_2] = \min(\alpha\mathbf p[v_1], 1) \pm \epsilon$ for real $\alpha \ge 0$, $\epsilon < 1$.
• Proposition 4.3: $\mathbf p[v_3] = \min(\alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2], 1) \pm \epsilon$ for real $\alpha, \beta, \gamma \ge 0$.
• Proposition 4.5 ($\mathcal G_\alpha$): $\mathbf p[v_1] = \min(\alpha, 1) \pm \epsilon$.
• Lemma 5.3 (comparator $\mathcal G_<$): $\mathbf p[d] = 1$ if $\mathbf p[a] < \mathbf p[b] - \epsilon$ and $\mathbf p[d] = 0$ if $\mathbf p[a] > \mathbf p[b] + \epsilon$.

Significance

The result. The paper reduces $r$-player games to three-player games by building a graphical game from gadgets, legally coloring it with three colors, and turning each color class into one player of a normal-form game (§4.2, §4.5). Proposition 4.18 supplies a gadget that computes $\min\{1, \alpha x + \beta y + \gamma xy\}$ and can be glued into such a construction while keeping it legally 3-colorable (p. 233), at the price of an error constant $81$ instead of the constant $1$ of the elementary gadgets. The error bound is what carries the reduction over to approximate equilibria: an $\epsilon$-Nash equilibrium of the gadget computes its function to within $81\epsilon$.

Formalizing it. All results here are proved in the paper (Proposition 4.5 is stated with the remark that its proof is similar to those of Propositions 4.2 and 4.3). None of them has a machine-checked proof, and no graphical-game or gadget infrastructure exists in Lean. The mission formalizes the known proofs and produces a library of verified gadgets with explicit error bounds, the first layer of any formal treatment of the PPAD-hardness of Nash equilibria.

Difficulty

Each claim is a case analysis on which strategy of an intermediate player is dominated by more than $\epsilon$, but the cases interact. Claim 3 needs Claims 1 and 2 as inputs, and it is the step where both $\alpha + \beta + \gamma \le 3$ and $\epsilon \le 0.01$ are used: without them one of the regimes of $w$ cannot be excluded. The three-strategy player $v_2'$ cannot be handled by the "binary player copies or disagrees" argument of the elementary gadgets; its weight on $1$ and on $*$ must be tracked separately. The error constants $10$ and $81$ propagate through products of approximate quantities, so a proof that is loose at any step does not reach them.

On the Lean side, the expected payoff of a pure strategy is a sum over all pure profiles of a ten-player game; every claim first has to reduce it to the few coordinates the player's payoff actually depends on.

Formalization scope

Games, mixed profiles and expected payoffs are those of the published agt_games bundle: a finite player type, strategy types S i, payoffs u : ι → (∀ i, S i) → ℝ, AGT.IsMixedProfile, AGT.expectedPayoff. The expected payoff of a pure strategy $j$ is the expected payoff of the profile with $p$'s strategy replaced by the point mass at $j$. An $\epsilon$-Nash equilibrium requires a genuine mixed profile.

Each gadget is one explicit game on its own player type, with the payoff tables of the paper. Binary strategies are Fin 2 with the paper's labels $0, 1$, and $\mathbf p[v]$ is the weight on 1; $v_2'$'s strategies are an inductive type {zero, one, star}. The input players' payoffs are unconstrained in the paper; here they are $0$, which makes the $\epsilon$-condition at the inputs vacuous. Since every non-input payoff depends only on gadget players, "$\epsilon$-Nash equilibrium of the standalone gadget" quantifies over all mixed strategies of the inputs and imposes the condition exactly on the other players, which is the paper's meaning when the gadget sits inside a larger game. The affects graph is computed from the payoff functions, without self-loops, and colors $\{1,\dots,k\}$ are Fin k. The ranges $\alpha, \beta, \gamma \in \mathbb N$ (Proposition 4.18) and $\alpha, \beta, \gamma \in \mathbb R_{\ge 0}$ (Propositions 4.2, 4.3, 4.5) follow the paper; $\epsilon \ge 0$ is added where the paper writes only $\epsilon < 1$.

The paper states Proposition 4.18 and Lemma 5.3 as "there is a graphical game"; an existential statement would be met by a game whose output has a dominant strategy and whose inputs are forced, so both are stated for the explicit game of the proof, with free inputs.

A complete development needs a computation lemma for the pure-strategy payoff in each gadget (reusable for any gadget on these definitions) and the case analyses of the claims. Proofs of the elementary gadgets, which are short, and of Claims 1 and 2 are good first contributions; Claim 3 is the main step.

Selected references

• C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM J. Comput. 39(1):195–259, 2009. https://doi.org/10.1137/070699652
• C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Comput. System Sci. 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7
• M. Kearns, M. L. Littman, S. Singh, Graphical Models for Game Theory, UAI 2001. https://arxiv.org/abs/1301.2281
• X. Chen, X. Deng, S.-H. Teng, Settling the complexity of computing two-player Nash equilibria, J. ACM 56(3):14, 2009. https://doi.org/10.1145/1516512.1516516

Motivation

A group of $m$ individuals each hold a subjective probability distribution over the same $n$ outcomes, and one wants a single distribution representing their consensus. Averaging and convolution are the obvious candidates. Eisenberg and Gale (Ann. Math. Statist. 30(1), 1959) observe that a real institution already performs such an aggregation: the pari-mutuel method of betting on horse races, in which the final "track's odds" on a horse are proportional to the total amount bet on it.

The difficulty is circular. Each bettor wants to bet where the ratio of their own probability to the track probability is largest, but the track probabilities are only known after everyone has bet. The paper asks whether track probabilities and bets compatible with both the bettors' strategies and the pari-mutuel principle exist, and whether they are determined by the data. It answers yes on both counts for the probabilities, which gives a well-defined notion of pari-mutuel consensus.

The variational problem the paper introduces, maximizing $\sum_i b_i \log(\text{utility}_i)$, is now known as the Eisenberg–Gale convex program. It is the standard tool for computing equilibria of linear Fisher markets, and the pari-mutuel market is the special case in which every bettor's utility for a horse is their subjective win probability.

Setting

There are $m$ bettors $B_1,\dots,B_m$ and $n$ horses $H_1,\dots,H_n$.

• The subjective probability matrix $P=(p_{ij})$ is $m\times n$; $p_{ij}$ is the probability, in the opinion of $B_i$, that $H_j$ wins. Each row is a probability distribution: $p_{ij}\ge 0$ and $\sum_j p_{ij}=1$.
• Bettor $B_i$ has a budget $b_i>0$, with the unit of money chosen so that $\sum_i b_i=1$.
• Each column of $P$ contains at least one positive entry (a horse nobody believes in can be removed).

Unknowns are Greek. $\pi_j$ is the track probability of $H_j$ and $\beta_{ij}$ is the amount $B_i$ bets on $H_j$. Nonnegative $\pi_j,\beta_{ij}$ are equilibrium probabilities and bets when

$$\text{(1)}\ \sum_{j=1}^n\beta_{ij}=b_i,\qquad \text{(2)}\ \sum_{i=1}^m\beta_{ij}=\pi_j,\qquad \text{(3)}\ \text{if } \mu_i=\max_s\frac{p_{is}}{\pi_s}\text{ and }\beta_{ij}>0,\text{ then }\mu_i=\frac{p_{ij}}{\pi_j}.$$

(1) is the budget relation, (2) the pari-mutuel condition, and (3) says each bettor bets only on horses that maximize the subjective expectation $p_{ij}/\pi_j$.

The paper's variational problem is

$$\varphi(\xi)=\sum_{i=1}^m b_i\log\sum_{j=1}^n p_{ij}\xi_{ij}\quad\text{on}\quad D=\Big\{\xi:\ \xi_{ij}\ge0,\ \sum_{i=1}^m\xi_{ij}=1\ \text{for all } j\Big\},$$

with $\varphi=-\infty$ where an inner sum vanishes. From a maximizer $\bar\xi$ it builds $\pi_j=\max_i b_ip_{ij}/\sum_s p_{is}\bar\xi_{is}$ (6) and $\beta_{ij}=\bar\xi_{ij}\pi_j$ (7). In Lean the market is PariMutuel.Consensus.Market m n, equilibrium is Market.IsEquilibrium, and $\varphi$, $D$, the maximizer predicate, (6) and (7) are Market.phi, D m n, Market.IsPhiMaximizer, Market.trackProb, Market.bets.

Formalization targets

Goal: existence and uniqueness of equilibrium probabilities

$$\exists!\,\pi\in\mathbb R^n\ \ \exists\,\beta\in\mathbb R^{m\times n}:\ (\pi,\beta)\ \text{are equilibrium probabilities and bets}.$$

Only $\pi$ is unique; the paper notes that equilibrium bets need not be.

Milestones

1. $\varphi$ attains its maximum on $D$ at a point with every inner sum positive (p. 167).
2. $\partial\varphi/\partial\xi_{ij}=b_ip_{ij}/\sum_s p_{is}\xi_{is}$ wherever the inner sums are positive (p. 167).
3. (8): at a maximizer, $\bar\xi_{ij}>0$ implies $\pi_j=\partial\varphi/\partial\bar\xi_{ij}$ (p. 167).
4. Every $\pi_j$ of (6) is positive (p. 167).
5. EXISTENCE THEOREM: for every maximizer $\bar\xi$, (6)–(7) are equilibrium probabilities and bets (p. 167).
6. Every equilibrium has $\pi_j>0$ (p. 168).
7. For two equilibria, $\sum_k\bar\pi_k\bar\pi_k/\pi_k\le 1$ (p. 168).
8. If $\pi>0$, $\bar\pi\ge0$, both sum to 1 and $\sum_k\bar\pi_k^2/\pi_k\le1$, then $\bar\pi=\pi$ (p. 168).
9. UNIQUENESS THEOREM: equilibrium probabilities are unique (p. 168).

A further, non-milestone item states the referee's example (p. 168): with two bettors of equal budgets and two horses, if the first bettor's distribution is $(\tfrac12,\tfrac12)$, the equilibrium probabilities are $(\tfrac12,\tfrac12)$ whatever the second bettor believes.

Significance

The result makes pari-mutuel odds a well-defined function of the bettors' beliefs and budgets, so the consensus can be studied as a mathematical object; the referee's example shows it behaves very differently from averaging, since a single indifferent bettor can fix it. The existence proof replaces a fixed-point argument by a concave maximization, which is the origin of the Eisenberg–Gale program, later the basis of convex-programming and combinatorial algorithms for Fisher market equilibria.

The theorems are classical and fully proved in the paper. To the knowledge of this mission they have no machine-checked proof. The mission produces a formal pari-mutuel market model, the Eisenberg–Gale program with the correct treatment of $\log 0=-\infty$, and Lean proofs of existence and uniqueness. The platform's Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities missions (Vazirani–Yannakakis) concern a related Fisher-market model with rational piecewise-linear utilities.

Difficulty

The existence statement, as the paper proves it, has two delicate points. $\varphi$ is $-\infty$ on part of the boundary of $D$, so "continuous on a compact set" needs the extended-real reading, and a real-valued formalization must handle the boundary separately. The first-order condition (8) has to be derived from maximality on a polytope with equality constraints on columns, not from an unconstrained critical point.

For uniqueness, the natural first idea, strict concavity of $\varphi$, fails: $\varphi$ is concave but not strictly concave in $\xi$, and indeed equilibrium bets are not unique. Uniqueness has to be proved for the probabilities directly, for arbitrary equilibria and not only those built from a maximizer, and it needs positivity of all $\pi_j$, which the paper uses without proof.

Formalization scope

• Bettors are Fin m and horses Fin n, indexed from 0. All data are real. Every standing assumption (rows of $P$ are probability vectors, no zero column, $b_i>0$, $\sum_i b_i=1$) is a field of Market; $m\ge1$ follows from $\sum_ib_i=1$.
• Condition (3) is written multiplied out: $\beta_{ij}>0\Rightarrow p_{is}\pi_j\le p_{ij}\pi_s$ for all $s$. This equals (3) when $\pi>0$ and encodes the paper's $p/0=+\infty$ when some $\pi_s=0$. Positivity of $\pi$ is not part of the definition of equilibrium; it is milestone 6.
• $D$ has column sums one, as in (5).
• $\varphi$ is real-valued. A maximizer is a point of $D$ with positive inner sums that dominates every point of $D$ with positive inner sums; the excluded points have $\varphi=-\infty$ on the page. The max in (6) is Finset.sup' over the nonempty set of bettors.
• Ruled out: a version of (3) with real division ($x/0=0$) admits spurious equilibria with $\pi_s=0$ and makes uniqueness false; a maximizer defined with the raw real $\varphi$ ($\log0=0$) changes the set of maximizers; adding $\pi>0$ or $\sum_j\pi_j=1$ to the equilibrium definition weakens the goal.
• Needed infrastructure: compactness of $D$ and an argument handling the $-\infty$ boundary, one-variable derivatives of $\log$ of linear forms, and the equality case of the Cauchy–Schwarz inequality. Milestones 7–9 use no analysis and can be attacked independently of 1–5. Proofs of any milestone, and reusable lemmas on the Eisenberg–Gale program, are welcome.

Selected references

• E. Eisenberg and D. Gale, Consensus of subjective probabilities: the pari-mutuel method, The Annals of Mathematical Statistics 30(1):165–168, 1959. https://doi.org/10.1214/aoms/1177706369
• V. V. Vazirani and M. Yannakakis, Market equilibrium under separable, piecewise-linear, concave utilities, Journal of the ACM 58(3), 2011. https://doi.org/10.1145/1970392.1970394

Motivation

Selfish routing and resource sharing are modelled by congestion games: each player picks a set of shared resources, and the cost of a resource grows with the number of players using it. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures how much worse the social cost of a worst Nash equilibrium is than the optimum. For non-atomic (infinitesimal) traffic with linear latencies, Roughgarden and Tardos (J. ACM 2002) showed the ratio is $4/3$. Christodoulou and Koutsoupias (STOC 2005) turned to finite (atomic, unweighted) congestion games, where each of $N$ players controls one indivisible unit of load, and determined the pure price of anarchy for linear latencies in four settings: asymmetric or symmetric strategy sets, and average or maximum social cost. Awerbuch, Azar and Epstein (STOC 2005) obtained the value $5/2$ for the asymmetric average case independently.

This mission covers the symmetric average-cost entry of that table (Sect. 3.2 of the paper). It shows that when all players share one strategy set, the ratio is not $5/2$ but $(5N-2)/(2N+1)$, which depends on the number of players and tends to $5/2$ only as $N\to\infty$.

Setting

A congestion game has a finite set of players $N=\{1,\dots,n\}$ (in Lean, Fin N), a finite set of facilities $E$, for each player $i$ a collection of pure strategies $\Sigma_i\subseteq 2^E$, and for each facility a latency $f_e:\mathbb N\to\mathbb R$. A profile $A=(A_1,\dots,A_n)$ picks $A_i\in\Sigma_i$ for each player (IsProfile). The load $n_e(A)$ is the number of players whose strategy contains $e$ (load), the cost of player $i$ is

$$c_i(A)=\sum_{e\in A_i} f_e\bigl(n_e(A)\bigr)$$

(cost), and the social cost is $\mathrm{SUM}(A)=\sum_i c_i(A)$ (sumCost), $N$ times the average cost. A profile $A$ is a pure Nash equilibrium (IsPureNash) if $c_i(A)\le c_i(A_{-i},S)$ for every player $i$ and every $S\in\Sigma_i$, where $(A_{-i},S)$ replaces $A_i$ by $S$.

Latencies are linear (IsLinear) when $f_e(k)=a_ek+b_e$ with $a_e,b_e\ge0$. The game is symmetric (IsSymmetric) when all players have the same strategy set, $\Sigma_i=\Sigma$. The pure price of anarchy of a class of games is the supremum, over games in the class and pure Nash equilibria $A$, of $\mathrm{SUM}(A)/\mathit{opt}$, with $\mathit{opt}=\min_P\mathrm{SUM}(P)$.

Formalization targets

Goal: Theorems 3 and 4

For every $N\ge1$: every pure Nash equilibrium $A$ of every symmetric linear congestion game with $N$ players satisfies

$$\mathrm{SUM}(A)\le\frac{5N-2}{2N+1}\,\mathrm{SUM}(P)\quad\text{for every profile }P,$$

and some symmetric linear game with $N$ players has a pure Nash equilibrium $A$ and a profile $P$ with $\mathrm{SUM}(P)>0$ and equality. Together these state that the pure price of anarchy of the class is exactly $(5N-2)/(2N+1)$.

Milestones

1. Lemma 1: $\beta(\alpha+1)\le\frac13\alpha^2+\frac53\beta^2$ for nonnegative integers $\alpha,\beta$.
2. Theorem 3, proof: the Nash inequality of player $i$ against the strategy $P_j$ of any player $j$.
3. Theorem 3, proof: the bound on $N\,c_i(A)$ obtained by summing over $j$.
4. Theorem 3, proof: the bound on $\mathrm{SUM}(A)$ obtained by summing over $i$.
5. Theorem 3: the upper bound alone.
6. Theorem 4: the matching instances alone.

Significance

The result separates symmetric from asymmetric games for every finite number of players: for $N=2$ the symmetric bound is $8/5$, for $N=3$ it is $13/7$, against $5/2$ for asymmetric games with $N\ge3$ players. Theorem 4 shows the bound is tight, so the function $N\mapsto(5N-2)/(2N+1)$ is the exact answer, not an artefact of the proof. The asymptotic value $5/2$ coincides with the asymmetric one, which says that symmetry helps only by a vanishing amount for large populations. Later work on smoothness arguments (Roughgarden, STOC 2009) takes the $5/2$ bound of this paper as its central example.

The theorems are proved in the paper; the authors print the proofs for identity latencies $f_e(k)=k$ and state that they extend to $a_ek+b_e$. No machine-checked proof of these bounds is known to exist. This mission produces a statement for general affine latencies with nonnegative coefficients, the affine forms of the intermediate inequalities, and an explicit family of instances for every $N$, all of which are reusable for the other entries of the paper's table.

Difficulty

The upper bound requires combining the $N^2$ deviation inequalities (player $i$ against the strategy of each player $j$ in the comparison profile) and then bounding cross terms facility by facility; the step that needs care is that the bound of Lemma 1 holds for integer loads only and fails for real numbers, so any argument that relaxes loads to reals loses the constant. The asymmetric argument, which compares player $i$ only with its own optimal strategy $P_i$, gives $5/2$ and cannot see the dependence on $N$.

For the lower bound, the instance must be a Nash equilibrium against every strategy in the common strategy set, which contains the equilibrium strategies of all other players as well as the optimal ones. Exact equality of the ratio requires the block sizes to be tuned to $N$; verifying the equilibrium condition involves counting facilities shared by pairs and triples of players.

Formalization scope

Players are Fin N with $N\ge1$; facilities are an arbitrary finite type with decidable equality; strategies and profiles are Finsets of facilities, with feasibility a separate predicate. Latencies are real-valued functions of the natural-number load. Linear latencies are affine with nonnegative coefficients, as in Sect. 2 of the paper; the milestone inequalities carry the coefficients $a_e,b_e$ explicitly and reduce to the printed displays when $a_e=1$, $b_e=0$. The Nash condition is in cost form. Upper bounds are stated against every feasible profile $P$, which is equivalent to the bound on $\mathrm{SUM}(A)/\mathit{opt}$ without dividing by $\mathit{opt}$. All constants are computed in $\mathbb R$.

The lower bound requires $\mathrm{SUM}(P)>0$: without it the statement is satisfied by zero latencies or empty strategies, where both sides vanish. Symmetry is a hypothesis of the upper bound and a property of the instance; without it the upper bound is false, since asymmetric instances reach $5/2$.

A complete development needs finite-sum manipulations (double counting $\sum_j\sum_{e\in P_j}=\sum_e n_e(P)$), the integer inequality of Lemma 1, and an explicit facility type for the instance. The model layer is shared with the other missions of this series. Proofs of the milestones and alternative proofs of the bound are welcome.

Selected references

• G. Christodoulou and E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar and A. Epstein, The Price of Routing Unsplittable Flow, Proc. 37th ACM STOC, 2005. https://doi.org/10.1145/1060590.1060599
• E. Koutsoupias and C. Papadimitriou, Worst-case Equilibria, STACS 1999. https://doi.org/10.1007/3-540-49116-3_38
• T. Roughgarden and É. Tardos, How Bad Is Selfish Routing?, J. ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
• T. Roughgarden, Intrinsic Robustness of the Price of Anarchy, Proc. 41st ACM STOC, 2009. https://doi.org/10.1145/1536414.1536485