Algorithmic Game Theory V: Stable Matching and Trading without Money

Motivation

When money is off the table and the Gibbard–Satterthwaite theorem (Mission III of this series) blocks general strategyproof choice, restricted preference domains reopen the door. The two great examples both come from allocation: Shapley–Scarf's housing market (1974), where Gale's Top Trading Cycle algorithm finds the unique core allocation and Roth (1982) showed the mechanism is strategy-proof; and the Gale–Shapley marriage market (1962), where deferred acceptance produces a stable matching, the men-optimal one, which Dubins–Freedman (1981) and Roth (1982) showed cannot be manipulated by any man. This machinery runs the US medical residency match and school choice systems worldwide, and the 2012 Nobel memorial prize to Roth and Shapley cites exactly the results of this mission. Chapter 10 (Schummer–Vohra, "Mechanism Design without Money") of Nisan–Roughgarden–Tardos–Vazirani (eds.), Algorithmic Game Theory (Cambridge, 2007) is the source text; its single-peaked §10.2 is left to a possible later mission, since it needs its own preference-domain machinery.

Setting

Marriage market (§10.4): finite sets $M$ of men and $W$ of women, each agent holding a strict preference ordering over the opposite side (the preference-profile vocabulary of Mission III; $P\,i\,a\,b$ reads "$i$ strictly prefers $a$ to $b$"). Following the book's dummy-partner convention, $|M| = |W|$ and a matching is a bijection $\mu : M \simeq W$. A pair $(m, w)$ blocks $\mu$ if each prefers the other to their assigned partner; $\mu$ is stable if no pair blocks it. A stable $\mu$ is male-optimal if every man weakly prefers it to every stable alternative. A coalition dominates $\mu$ if it can rematch within itself with every member strictly better off; the core is the set of undominated matchings.

Housing market (§10.3): a finite set $N$ of agents, agent $i$ owning house $i$, each with a strict preference over all houses; an allocation is a permutation of $N$. A coalition blocks an allocation if it can redistribute the houses its members own so that all are weakly and someone strictly better off.

Formalization targets

Goal (capstone) — Theorem 10.13

Any mechanism selecting the male-optimal stable matching is strategy-proof for the men: no man can misreport his ordering and obtain a wife he truly prefers.

Theorem 10.10 — existence

Every marriage market has a stable matching.

Theorem 10.11 / Gale–Shapley 1962 — male-optimality

Some stable matching is weakly best for every man simultaneously. This man-by-man form is Gale–Shapley's optimal assignment (1962, Theorem 2); the book's Theorem 10.11 phrases male-optimality as the absence of a stable alternative making every man weakly and some man strictly better off, which is equivalent for finite strict markets — the equivalence being a (short) theorem, the attribution follows Gale–Shapley.

Theorem 10.12 — the core

A matching is stable iff it is in the core of the matching game.

Theorems 10.6 and 10.7 — housing

The core of the housing market is a single allocation, and the mechanism selecting it is strategy-proof.

Significance

These are the foundational theorems of market design — the branch of mechanism design with the strongest record of deployed systems — and none of them exists in Lean. The mission also settles a methodological point for the series: algorithm-defined objects (deferred acceptance, top trading cycles) enter through the properties that characterize their outputs — male-optimality, core membership — so the theorems are statements about all mechanisms with the given property, and any construction of the algorithm proves the existence milestones. The matching vocabulary (bijections as matchings, blocking, stability, domination) is reusable for the college-admissions and roommates variants beyond this mission.

Difficulty

Existence (10.10) is the real formalization work: whether by formalizing deferred acceptance and its termination or by another route (e.g. Adachi's fixed-point formulation, which the book sketches as Theorem 10.14 via Tarski), the solver must build the proposal machinery. Male-optimality (10.11) rides on the same construction with the "no man is ever rejected by an achievable wife" invariant. The core equivalence (10.12) is deliberately light — a transposition embeds a blocking pair as a two-agent coalition. Housing uniqueness (10.6) needs the cycle-peeling induction of TTC. The two strategyproofness results are the subtle ones: both known proof routes (Dubins–Freedman's combinatorial argument, or Roth's via the blocking lemma) require careful bookkeeping of which coalitions can improve under a misreport, and the mechanism is pinned only by its defining property, so proofs must use optimality/core facts rather than algorithm internals.

Formalization scope

Preferences are strict total orders as in Mission III (IsPrefProfile), oriented "first argument preferred". Matchings are Equivs; the book's $|M| = |W|$ convention enters the existence statements as the hypothesis Nonempty (M ≃ W) and nothing else about cardinalities is assumed. Domination and house-blocking quantify a rematching Equiv together with the improving coalition, coalitions being sets closed under the rematching — single-agent and pair coalitions are special cases, so no separate pair-blocking clause is needed in the core theorems. Mechanisms in the strategyproofness results are arbitrary functions constrained only by their defining property (male-optimal selection; core selection), quantified before the misreport — nothing may be chosen with hindsight. Both sides keep finiteness only where used: the core equivalence (10.12) holds for arbitrary types and carries no Fintype.

Selected references

• D. Gale, L. S. Shapley, College admissions and the stability of marriage, Amer. Math. Monthly 69 (1962), 9–15. DOI
• L. Shapley, H. Scarf, On cores and indivisibility, J. Math. Econ. 1 (1974), 23–37. DOI
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley algorithm, Amer. Math. Monthly 88 (1981), 485–494. DOI
• A. E. Roth, The economics of matching: stability and incentives, Math. Oper. Res. 7 (1982), 617–628. DOI
• A. E. Roth, Incentive compatibility in a market with indivisible goods, Econ. Letters 9 (1982), 127–132. DOI
• N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007, Chapter 10. DOI

Certify the classical quadratic separation between sensitivity and block sensitivity: $\alpha\ge2$.

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$, write $x^B$ for the input obtained by flipping the coordinates in $B$. Its sensitivity is $s(f)=\max_x|\{i:f(x^{\{i\}})\ne f(x)\}|$. Its block sensitivity $bs(f)$ is the largest number of pairwise disjoint nonempty sets $B$ that satisfy $f(x^B)\ne f(x)$ at a common input $x$.

The goal is to prove that for every $\varepsilon>0$ and every integer $S\ge2$, there is a total Boolean function with

$$s(f)\ge S,\qquad bs(f)\ge s(f)^{2-\varepsilon}.$$

The construction milestone is Rubinstein’s quadratic separation: for each integer $m\ge1$, there is a function on $(2m)^2$ bits with

$$s(f)=2m,\qquad bs(f)=2m^2.$$

These exact bounds imply the goal because $bs(f)=s(f)^2/2$ and sensitivity grows without bound. This is a known theorem; the task is to formalize it using the campaign’s shared definitions.

The main combinatorial work is controlling sensitivity at every input and proving the matching block-sensitivity bounds. Lean represents functions as (Fin n → Bool) → Bool; both measures are maxima over all inputs. The goal reuses SensitivityCampaign.AchievesExponent, so it has exactly the same meaning as the campaign’s stronger targets. No composition theorem is required for this family argument.

References: David Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica 15 (1995), 297–299, DOI. The statement and construction are also recalled in Theorem 1 of Madars Virza, Sensitivity versus block sensitivity of Boolean functions (2010), arXiv:1008.0521.

Motivation

In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent $i$ holds a private signal $s_i$, and every agent's value is a publicly known function of the whole signal profile $\mathbf s=(s_1,\dots,s_n)$.

With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor $n$ (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking $k$ values.

Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, $c$-single-crossing condition, with ratios depending on $c$ and $n$. Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.

Setting

There are $n$ agents and $m$ items, and $k\ge1$ signal values. Each agent $i$ has a signal $s_i\in\{0,1,\dots,k-1\}$, and $\{0,\dots,k-1\}^n$ is the grid. Agent $i$'s value for a bundle $T\subseteq[m]$ at the profile $\mathbf s$ is $v_{iT}(\mathbf s)\ge0$; the empty bundle is worth $0$, and for nonempty $T$, $v_{iT}$ is weakly increasing in every signal and strictly increasing in $s_i$. We write $(\mathbf s_{-i},x_i)$ for the profile with agent $i$'s signal replaced by $x$, and $(\mathbf s_A,\mathbf 0_B)$ for the profile that keeps the signals of the agents in $A$ and sets those in $B$ to $0$.

A function $w$ of the profile is SOS if for every coordinate $j$, all $x,\delta\ge0$ with $x+\delta\le k-1$, and grid profiles with $\mathbf s'_{-j}\le\mathbf s_{-j}$ coordinatewise,

$$w(\mathbf s_{-j},x+\delta)-w(\mathbf s_{-j},x)\;\le\;w(\mathbf s'_{-j},x+\delta)-w(\mathbf s'_{-j},x).$$

The setting is SOS when every $v_{iT}$ is.

A feasible allocation gives disjoint bundles $T_1,\dots,T_n$; its welfare at $\mathbf s$ is $\sum_i v_{iT_i}(\mathbf s)$. A deterministic mechanism maps reported profiles to an allocation and payments. Agent $i$'s utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

The mechanism k-HL runs, with probability $p_{RT}=\frac{k-1}{k+3}$, Random Threshold: choose $\ell$ uniformly in $\{1,\dots,k-1\}$, call $N_{\ge\ell}=\{i:s_i\ge\ell\}$ the high agents, allocate to them a feasible allocation maximizing $\sum_{i\in N_{\ge\ell}}v_{iS_i}(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$, and charge agent $i$ receiving $\bar T_i$ the price $v_{i\bar T_i}(\mathbf s_{-i},s_i=\ell-1)$. Otherwise it runs Random Sampling: split the agents uniformly at random into $A$ and $B$, allocate to $B$ a feasible allocation maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$, and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.

Formalization targets

Goal: Theorem 6.1 (p. 20)

For SOS valuations with $k$ signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile $\mathbf s$ and every feasible allocation $T^*$,

$$\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(k+3)\,\mathbb E\bigl[\text{welfare of k-HL at }\mathbf s\bigr],$$

where the expectation is over $\ell$, over $(A,B)$ and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.

Milestones

1. Displays (6)–(7): the welfare of any allocation is at most $\mathsf{OTHER}+\mathsf{SELF}$, where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ and $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$.
2. Random Sampling is ex-post IC-IR for every partition.
3. Random Threshold is ex-post IC-IR for every threshold.
4. Lemma 6.2: $\mathsf{SELF}\le(k-1)\,\mathbb E[\text{welfare of Random Threshold}]$.
5. Lemma 6.3: $\mathsf{OTHER}\le4\,\mathbb E[\text{welfare of Random Sampling}]$.

Significance

Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio $k+3$ depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the $(2\log_2k+4)$-approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.

The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.

Difficulty

Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within $\{\ell,\dots,k-1\}$ leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data $(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid $\{0,\dots,k-1\}^n$, with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in $A$ receive nothing, agents outside $N_{\ge\ell}$ receive nothing) must match the mechanism exactly.

Formalization scope

Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below $k$; a condition on all of $\mathbb N^n$ would be stronger than the paper's. The empty bundle is worth $0$ and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive $\emptyset$.

The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of $B$) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, $\frac1{k-1}\sum_{\ell=1}^{k-1}$ and $2^{-n}\sum_{B\subseteq[n]}$, never an existential or universal quantifier over $\ell$ or $B$. The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of $B$, the agent's own included (the page's "$v_{ij}(\mathbf s_A,\mathbf 0_B)$" is read as $v_{iT}(\mathbf s_A,\mathbf 0_B)$). For $k=1$, $p_{RT}=0$ and the threshold average is the empty sum.

Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing $T^*$.

Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.

The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
• A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, ACM EC 2018 (cited as [Eden et al., 2018] in the source).
• E. Maskin, Auctions and Privatization, in H. Siebert (ed.), Privatization, 1992 (cited as [Maskin, 1992] in the source).
• P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737
• P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00248

Motivation

In the secretary problem $n$ candidates arrive one at a time in uniformly random order; at each arrival the decision maker sees only how the current candidate compares with the earlier ones and must accept or reject irrevocably, aiming to accept the best candidate overall. Dütting, Lattanzi, Paes Leme and Vassilvitskii, Secretaries with Advice (arXiv:2011.06726), study a family of variants in which each candidate also carries a signal about its quality, and show that for many of them the optimal stopping rule is the solution of a finite factor-revealing linear program whose dual can be solved greedily by backward induction.

One of their main examples is the secretary problem with samples: before the $n$ candidates arrive, $k$ further elements of the same random order are revealed as a sample, and a candidate's signal is the number of sample elements smaller than it. This model interpolates between the classical problem ($k=0$, optimal success probability tending to $1/e$) and, as $k\to\infty$, the full-information problem of Gilbert and Mosteller (1966). The paper's Theorem 17 gives the optimal dual solution of this LP in closed form.

Setting

Fix natural numbers $n\ge 1$ (secretaries) and $k\ge 0$ (samples). Rounds are $i=1,\dots,n$; signals are $s\in\{0,1,\dots,k\}$. The dual LP of §5 has the coefficients

$$a(i,s)=\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{s+t}{k+t+1},\qquad c(j,s',i,s)=\frac{1}{s'+1}\prod_{t=1}^{i-1}\frac{s+t}{s'+t+1}\ \ (s'\ge s),$$

with $c(j,s',i,s)=0$ for $s'<s$, and reads

$$\min\sum_{i}\sum_{s}u(i,s)\quad\text{s.t.}\quad u(i,s)+\sum_{j>i}\sum_{s'\ge s}u(j,s')\,c(j,s',i,s)\ge a(i,s),\quad u(i,s)\ge 0 .$$

The greedy solution (equation (8) of the paper) sets $u(n,s)=a(n,s)$ and, going backwards,

$$u(i,s)=\max\Bigl\{0,\ a(i,s)-\sum_{j>i}\sum_{s'}u(j,s')\,c(j,s',i,s)\Bigr\}\qquad(i<n).$$

The un-clipped recursion $v(i,s)$ is the same backward induction with the $\max\{0,\cdot\}$ removed. In Lean, the generic recursion (8) is greedyDual (and unclippedDual) over an arbitrary finite signal type, and the samples instance is samplesGreedy n k i s (resp. samplesUnclipped) with s : Fin (k + 1). Products $\prod_{t=a}^{b}$ with $b<a$ equal $1$.

Formalization targets

Goal: Theorem 17

For every $1\le i\le n$ and $0\le s\le k$: $u(n,s)=a(n,s)$, and for $i<n$

$$u(i,s)=\max\left\{0,\frac{1}{k+1}\prod_{t=1}^{i-1}\frac{s+t}{k+t+1}\left(\prod_{t=i}^{n-1}\frac{s+t}{k+t+1}-\frac{\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{\ell=1}^{n-i-j}(s+i-1+\ell)}{\prod_{t=i}^{n-1}(k+t+1)}\right)\right\}.$$

Milestones (the steps of the paper's proof)

1. Reduction (p. 17): if $v(i',\cdot)$ has the closed form for all $i'>i$, then $v(i,s)=a(n,s)-\frac{1}{k+1}\prod_{t=1}^{n-1}\frac{1}{k+t+1}\prod_{t=1}^{i-1}(s+t)\sum_{s'=s}^{k}T(i,s')$, with $T(i,s')$ an explicit double sum.
2. Two forms of $T$ (pp. 17–18): the double sum collapses to $\sum_{j=1}^{n-i-1}(n-i)\binom{n-i-1}{j}\frac{1}{j(j+1)}\prod_{\ell\le j}(k-s'+\ell)\prod_{t=i+1}^{n-j-1}(s'+t)$.
3. Key identity (p. 18): $\sum_{s'=s}^{k}T(i,s')=\sum_{j=1}^{n-i}\binom{n-i}{j}\frac1j\prod_{\ell=1}^{j}(k-s+\ell)\prod_{t=i}^{n-j-1}(s+t)$.
4. Base case $s=k$ (p. 18) and 5. inductive step $s+1\to s$ (Appendix B, pp. 26–28) of the key identity.
5. Un-clipped closed form (pp. 17–19): $v(i,s)$ equals the expression inside the max, for all $1\le i\le n$.

Significance

Theorem 16 of the paper shows that the greedy dual solution is optimal and that the optimal policy for secretaries with samples is a threshold policy in the signal: accept a best-so-far candidate in round $i$ iff its signal is large enough. Theorem 17 makes this solution explicit, so the optimal thresholds can be read off from the sign of a closed-form expression rather than computed by running the backward recursion, and it is the discrete precursor of the paper's Corollary 18, which recovers the Gilbert–Mosteller full-information thresholds in the limit $k\to\infty$.

The identities are proved in the paper by explicit manipulation of finite sums and products of binomials. No machine-checked version exists. A formal proof checks the long index computations of the proof and of Appendix B, and closes a gap: the paper proves the identity for the un-clipped recursion only ("for the proof we can ignore the $\max\{0,\cdot\}$") and does not argue why the clipped greedy solution has the same form. The goal as stated here, with the maximum, is the statement the paper asserts.

Difficulty

The identities are rational-function identities in $s$, $k$ and the round indices, with sums whose ranges depend on the summation variables and products whose ranges may be empty. The natural first idea, induction on $n-i$ directly on the formula, requires the key identity for $\sum_{s'=s}^{k}T(i,s')$, a double sum over $s'$ and $j$ of products of rising factorials; the paper handles it by a second backward induction over $s$, and both the base case and the step re-index sums with shifted bounds and boundary terms such as $(n-i-1)!$ and $\frac{1}{n-i}\prod_{\ell=1}^{n-i}(k-s+\ell)$.

The passage from the un-clipped to the clipped recursion is a separate difficulty: once $u(j,s')$ is clipped to $0$ at a later round, the sums used at earlier rounds differ from those of the un-clipped recursion, and the closed form survives only because the clipped entries do not affect the relevant sums. That argument is not in the paper.

Formalization scope

• Rounds are natural numbers $1\le i\le n$ (1-based, as printed); signals are Fin (k + 1) in the recursion and naturals $s\le k$ in the formulas. All arithmetic is in $\mathbb R$; naturals are cast before $k-s$, and the natural differences $n-i$, $n-i-j$, $n-j-1$ appear only where the ranges keep them non-truncated.
• Products and sums are over Finset.Icc a b, empty when $b<a$, matching the paper's convention.
• The recursion is defined by well-founded recursion on $n-i$ and sums over all later rounds $j\in\{i+1,\dots,n\}$ and all signals; $c=0$ for $s'<s$ encodes the paper's $\sum_{s'\ge s}$.
• The goal keeps the $\max\{0,\cdot\}$. Stating instead the identity for the un-clipped recursion would be a different (weaker-content) theorem; it is milestone 6.
• No probability model appears: the coefficients are taken as given by their formulas on p. 15. Their probabilistic derivation, the optimality of the greedy solution (Theorem 16), the running time of the LP algorithm, the "natural interpretation" paragraph, Corollary 18 and the plots are out of scope.
• The generic recursion greedyDual is reusable for any instance of the paper's factor-revealing LP (the binary-classifier model of §6 included). General lemmas about sums of rising factorials (ascPochhammer) and binomial re-indexing developed for the milestones are welcome contributions.

Selected references

• P. Dütting, S. Lattanzi, R. Paes Leme, S. Vassilvitskii, Secretaries with Advice, arXiv:2011.06726v1, 2020; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2011.06726
• J. P. Gilbert, F. Mosteller, Recognizing the Maximum of a Sequence, Journal of the American Statistical Association 61(313), 1966. https://doi.org/10.1080/01621459.1966.10502008
• T. S. Ferguson, Who Solved the Secretary Problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493

Verified completion - 15 October 2026

The original exact goal EndStatement.ThreeSum.SolvedInTime 1.960614 is Proved on Prove2Me. All seven original milestones are complete. The complete machine extension has 481 accepted theorem proofs and reuses 110 proved theorem nodes; its accepted dependencies connect to the original main reduction. The independent fixed-model lower bound remains separate from the algorithm proof. Scientific priority and global optimality are not asserted by these formal verification results.

Why improve the deterministic integer 3SUM exponent?

3SUM asks whether three entries at distinct positions in an integer input sum to zero. Its familiar quadratic algorithm makes it a benchmark for studying how much arithmetic structure can reduce the cost of an exhaustive search. The relevant comparison is the exponent of input size in a precisely specified machine model. An improvement to that exponent is an asymptotic statement; it need not provide better measured running times at accessible input sizes.

Alman and Vassilevska Williams, 2026 developed a deterministic truly subquadratic framework for polynomially bounded integer 3SUM. The c0ldzy17 source snapshot, dated 11 October 2026, develops a subsequent deterministic construction with a formally stated 1.962 target. The author-supplied certificate package 3sum_certificate_1p960614_v3, dated 14 October 2026, studies a further parameter and switch refinement. It contains mathematical arguments and exact rational checks, and explicitly leaves the complete modified machine-program theorem unproved. This mission studies that remaining extension together with its supporting certificates.

Inputs, word instructions and analytic quantities

An input of size $n$ is an integer-valued function on the positions $0,\ldots,n-1$. For each fixed natural number $\kappa$, every value has absolute value at most $n^\kappa$. A YES instance has pairwise distinct positions $i,j,k$ satisfying $x_i+x_j+x_k=0$. Equal values at different positions are allowed. The problem asks for a decision, so a successful algorithm need not return the positions. Inputs of size less than three are NO instances.

The word RAM is the existing campaign foundation specification. A program is a finite list of instructions for constants, arithmetic, direct and indirect memory access, branching, acceptance and rejection. Words have a fixed width and a signed integer interpretation. For each fixed $\kappa$, one program, one word-width constant and one time function must work for every input size and every sufficiently large word width. The mission retains that specification without introducing an alternative computation model.

The supporting binary entropy is measured in bits:

$$H(t)=\frac{-t\log t-(1-t)\log(1-t)}{\log2},\qquad H(0)=H(1)=0.$$

For an integer expansion $c\ge3$, write

$$E_c=\frac c2H(1/c),\quad \kappa_c=2cH(1/(2c))-cH(1/c)-1,\quad \gamma_c(t)=cH(1/c)-cH((1-t)/c).$$

These are analytic quantities used to describe local encoding and reporting costs. The source's twelve charges also depend on a representation-scale parameter $e$, a band shift $b$, a box saving $S$, an initial threshold $\theta$, a terminal fraction $\tau$, and a uniform entropy coefficient $\rho$.

Formalization targets

The campaign goal is the exact proposition

$$\texttt{EndStatement.ThreeSum.SolvedInTime}\;(1.960614).$$

For $1.960614=980307/500000$, its time requirement is

$$\exists K\in\mathbb N\;\forall n\ge2,\quad T(n)^{500000}\le K n^{980307}.$$

Correctness and termination still cover all input sizes. The integer-size exponent includes $\kappa=0$, and the same program must be correct for every word width above its specified threshold.

The primary certificate uses $c=232$ and the rational quartic

$$P(t)=7.85174904t+0.72447023t^2+0.24044466t^3+0.12022459t^4.$$

Supporting targets establish its validity on $[0,1/2]$, its derivative and tangent bounds, and the uniform inequality $H(t)<0.27905030(1+P(t))$. The fixed parameters are $e=0.203889696$, $b=-0.062656016$, $S=0.193175570$, $\theta=0.040409899$, and $\tau=13/20$. The parameter theorem bounds every one of the twelve costs strictly below $1.96061388<1.960614$. Integer scheduling and general local-cover identities are separate milestones. A further independent milestone proves $R>1.96061349120$ for the explicitly defined relaxed fixed-expansion cost model. That model bound concerns its admissible parameter tuples; it is not a lower bound for 3SUM itself.

What these results establish

The supplied certificate demonstrates that a quartic switch already suffices for the proposed 1.960614 cost target. It also separates a uniform analytic inequality from a numerical experiment: the statement quantifies over the full closed interval. Its finite scheduling statement uses integer comparisons and accounts for the rounding error at every admissible level, rather than requiring executable logarithms.

Formalization adds checked statements about these continuous and finite objects and a reusable dependency structure. The full campaign goal requires an additional result: the actual modified program must obey the certified costs, and its operational correctness must reach the foundation specification. The upstream parameter certificate likewise distinguishes its exponent ledger from its separate implementation obligations. An exact rational checker passing is evidence for the numerical certificates; it does not establish the full new machine theorem.

Why the program extension remains substantive

Changing expansion from 256 to 232 changes the local universe and the vertex, output and degree counts together. The representation scale, band denominator and polynomial switch also change. Consequently, the original fixed-parameter runtime result cannot simply be invoked after replacing a few numerical constants. The new local construction, global encoding, sparse queries, reporting and arithmetic operations must share consistent parameters and a complete cost account.

The small gap between the principal cost cap and the target must absorb the proved subpolynomial overheads, including exceptional-size handling and the conversion to word instructions. The machine bridge has now been proved in this mission. Its accepted dependency tree connects the modified program and its runtime analysis to the unchanged campaign specification. Its statement has no assumed solver callback or unproved runtime contract. The fixed-model lower-bound milestone is an independent analytic root, and is not used to justify a faster algorithm.

Formalization scope and source boundaries

The campaign pins Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Entropy and its derived quantities are real-valued; the final exponent is rational; finite subset counts and cleared switch comparisons use natural numbers. Theorems explicitly restrict logarithmic arguments and denominators to their intended domains. Natural-number subtraction in the switch is used only below the final level, with positive even microblock size.

The local-cover milestone covers every natural $c\ge3$ and positive half-block size. The cost-model milestone quantifies over all tuples satisfying its written assumptions and includes a whole-interval entropy constraint. Neither finite testing nor a floating-point optimizer substitutes for these universal statements. The initial package includes no Lean proof of the new machine goal, and the mission does not represent it as an established record.

The underlying algorithms and formal infrastructure retain their attribution to Alman and Vassilevska Williams; Björklund, Husfeldt, Kaski and Koivisto; Swapnil Jain; c0ldzy17; Anthropic; Jihoon Hyun; and Lean/Mathlib, as documented by the upstream source. The certificate development and this formalization use AI assistance. Scientific priority and global optimality are outside the mission's claims.

Selected references

• Author-supplied 3SUM: Positive-Coefficient Entropy Switch, 1.960614 Cost Certificate and Fixed-Model Lower Bound, certificate package v3, 14 October 2026. Exact source: 3sum_certificate_1p960614_v3/3sum_certificate_v3/PROOF.md, Sections 0–8; certificates/c232_quartic.json; verify_certificate.py. This is a supplied research artifact, not a claimed public publication.
• c0ldzy17, Deterministic 3SUM in O(n^1.962): method and proof, source documentation, 2026. Pinned METHOD.md, Parameters.lean, and LocalCoverBounds.lean.
• Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, arXiv preprint, 2026. arXiv:2610.06783v1.
• Anthropic, Truly Subquadratic 3SUM and Truly Subcubic APSP, Lean formalization, 2026. Pinned formal-math source. The campaign imports its shared word-RAM statement.

Source code and complete Lean formalization: GitHub repository. Fixed source revision: 8c25c0325de5.

Motivation

An error-correcting code stores or transmits messages as words over a finite alphabet, adding redundancy so that the original word can be recovered after some symbols are corrupted. The basic question of coding theory is the trade-off between the amount of redundancy and the number of errors that can be corrected. The Hamming bound (also called the sphere-packing bound) is the first and most widely taught upper limit on this trade-off. It is due to R. W. Hamming (1950), who introduced the Hamming distance and the Hamming codes in the same paper (Hamming 1950).

This mission formalizes the bound as it is stated in Theorem 1.7.2 of the textbook Essential Coding Theory by V. Guruswami, A. Rudra and M. Sudan (web draft, §1.7, p. 21). It is the first mission of a series following that book. The result is used throughout the book to define perfect codes (Definition 1.7.3) and as the baseline against which later bounds (Singleton, Plotkin, Elias–Bassalygo, the linear-programming bound) are compared.

Setting

Let $\alpha$ be a finite alphabet with $q = |\alpha|$ symbols, and let $n \ge 0$. A word of length $n$ is a function $\{0, \dots, n-1\} \to \alpha$, and $\alpha^n$ is the set of all $q^n$ words. A code of block length $n$ is a subset $C \subseteq \alpha^n$; its elements are codewords.

The Hamming distance $\Delta(u, v)$ between two words is the number of coordinates in which they differ. The dimension of $C$ is the real number $k = \log_q |C|$ (Definition 1.2.3 of the book). The book calls $C$ an $(n, k, d)_q$ code when its minimum distance $\min_{c_1 \ne c_2 \in C} \Delta(c_1, c_2)$ equals $d$ (Definitions 1.4.1 and 1.7.1).

The Hamming ball of radius $e$ around a word $x$ is $B(x, e) = \{ y \in \alpha^n : \Delta(x, y) \le e \}$ (Definition 1.6.1).

Formalization targets

Milestone: volume of a Hamming ball

For every word $x \in \alpha^n$ and every radius $e \ge 0$,

$$|B(x, e)| = \sum_{i=0}^{e} \binom{n}{i} (q-1)^i.$$

This is equation (1.18) in the book.

Goal: the generalized Hamming bound

If any two distinct codewords of $C \subseteq \alpha^n$ are at Hamming distance at least $d$, then

$$\log_q |C| \;\le\; n - \log_q \Bigl( \sum_{i=0}^{\lfloor (d-1)/2 \rfloor} \binom{n}{i} (q-1)^i \Bigr).$$

The hypothesis is "minimum distance at least $d$" rather than "exactly $d$". Every $(n, k, d)_q$ code satisfies it, so the goal contains the book's Theorem 1.7.2 as stated.

Significance

The result itself. The bound says that a code correcting $\lfloor (d-1)/2 \rfloor$ errors can have at most $q^n / \mathrm{Vol}_q(\lfloor (d-1)/2 \rfloor, n)$ codewords, so its rate is at most $1 - \log_q \mathrm{Vol}_q / n$. Codes meeting it with equality are the perfect codes: the Hamming codes, the binary repetition codes of odd length, and the two Golay codes. The bound's asymptotic form, $R \le 1 - H_q(\delta/2)$, is one of the standard upper bounds on the rate–distance trade-off and is the reference point for the stronger bounds later in the book.

Formalizing it. The theorem has been proved since 1950 and appears in every coding theory text. Mathlib has the Hamming distance (hammingDist) but no notion of a code's distance, no Hamming-ball cardinality formula, and no sphere-packing bound. This mission supplies those, with the dimension stated through the real logarithm exactly as in the book, so later missions in the series can cite it.

Difficulty

The mathematics is elementary. The work lies in the counting step: showing that exactly $\binom{n}{i}(q-1)^i$ words lie at distance exactly $i$ from a fixed word. This identity has no ready-made counterpart in Mathlib, and the alphabet carries no algebraic structure, so translating every ball to a ball around a fixed word is not available. The final step, taking $\log_q$ of both sides, must also handle the conventions of the real logarithm on degenerate inputs.

Formalization scope

• The alphabet is an arbitrary type α with [Fintype α] [DecidableEq α], and $q$ is Fintype.card α. Words are functions Fin n → α, and $\Delta$ is Mathlib's hammingDist.
• A code is a Finset (Fin n → α). The distance hypothesis quantifies over pairs of distinct codewords.
• The dimension is Real.logb q |C|, a real number. The ball volume is the natural-number sum $\sum_{i=0}^{\lfloor (d-1)/2 \rfloor} \binom{n}{i}(q-1)^i$, cast to $\mathbb{R}$, where $\lfloor (d-1)/2 \rfloor$ is computed in $\mathbb{N}$ as (d - 1) / 2.
• No hypotheses $q \ge 2$ or $C \ne \emptyset$ are imposed. The book assumes them tacitly. Under Lean's conventions $\log_q x = 0$ when $q \le 1$ or $x = 0$, and the statement remains true in those cases. It is therefore at least as strong as the book's version, and these degenerate cases are not a trivialization: for $q \ge 2$ and $C \ne \emptyset$ the goal is equivalent to the sphere-packing inequality $|C| \cdot \mathrm{Vol} \le q^n$.
• No custom definitions are needed. The ball-volume formula is reusable for any later bound that counts Hamming balls (Gilbert–Varshamov, Elias–Bassalygo). Contributions of alternative counting proofs are welcome.

Selected references

• V. Guruswami, A. Rudra and M. Sudan, Essential Coding Theory, draft textbook, §1.6–1.7, Theorem 1.7.2, p. 21. https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf
• R. W. Hamming, Error detecting and error correcting codes, Bell System Technical Journal 29(2), 147–160, 1950. https://doi.org/10.1002/j.1538-7305.1950.tb00463.x
• The Mathlib Community, hammingDist, Mathlib.InformationTheory.Hamming. https://leanprover-community.github.io/mathlib4_docs/Mathlib/InformationTheory/Hamming.html

Why sharpen the integer 3SUM exponent?

3SUM asks whether an input sequence contains three entries at different positions whose sum is zero. The classical quadratic running time makes it a benchmark for fine-grained algorithm design: even a small fixed improvement in the exponent changes its asymptotic complexity. The setting here is polynomially bounded integers and a deterministic word RAM; the input-size exponent, rather than an experimental speedup, is the quantity being studied.

Alman and Vassilevska Williams (2026) give a deterministic truly subquadratic integer 3SUM algorithm through thin matrix products and reductions involving Exact Triangle. Xu's manuscript, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, dated 13 October 2026, refines the analysis of that framework. Its claimed bound is the formalization target here. The Hexagon link identifies the author's submission page, which may require authentication; it is not presented as a public article identifier or evidence of peer review.

Inputs, machine model, and analytic quantities

An input of size $n$ is a function $x:\{0,\ldots,n-1\}\to\mathbb Z$. For a fixed natural number $\kappa$, every entry obeys $|x_i|\le n^\kappa$. Acceptance means that there are pairwise distinct indices $i,j,k$ with $x_i+x_j+x_k=0$. Repeated values at different positions are allowed. This is a decision problem, so the algorithm need not return a witness triple.

The word-RAM specification is the campaign's existing EndStatement definition, imported from its foundation mission. For each fixed $\kappa$, one finite deterministic program, one word-width threshold constant, and one time-bound function must work for all input sizes and all word widths above that threshold. Words have finite signed interpretations; arithmetic, indirect memory access, branching, acceptance, and rejection are defined operationally. The result concerns this exact model.

For the supporting analysis, let $H(u)=-u\log u-(1-u)\log(1-u)$, with endpoint values $H(0)=H(1)=0$. All logarithms are natural. For an integer $c>10$, a positive integer $m$, and $0<\theta<0.9$, set $L=cm$, $D=4^m$, $t=\lceil\theta m\rceil$, and

$$\beta_d=\binom L{m-d}9^{L-m+d},\qquad M=\beta_0.$$

The sharp preprocessing saving, query exponent, and encoding exponent are

$$\gamma_*(c,\theta)=\frac{cH(1/c)-cH((1-\theta)/c)-\theta\log9}{\log4},$$ $$q(\theta)=\frac{H(\theta)+\theta\log9}{\log4},\qquad A(c)=\frac{c\log10-cH(1/c)/2-(c-1)\log3}{\log4}.$$

These auxiliary definitions describe costs; they neither redefine 3SUM nor assume the existence of a fast algorithm.

Formalization targets

The campaign goal is the exact fixed bound

$$\texttt{EndStatement.ThreeSum.SolvedInTime}\;1.999017.$$

The first supporting milestone is the two-sided binomial entropy estimate. The second is the manuscript's normalized tail bound

$$\frac1M\sum_{d=t}^m\beta_d\le\frac{cm+1}{1-9/(c-1)}D^{-\gamma_*(c,\theta)}.$$

A further milestone establishes strict improvement over the earlier preprocessing saving $\gamma(c,\theta)=\theta\log((c-1)/9)/\log4$ at fixed parameters. The algorithmic milestone combines the manuscript's Propositions 4.1 and 5.1: admissible sharp-tail parameters must yield a program satisfying the shared 3SUM specification, not merely a numerical inequality.

The final supporting milestone certifies the exact choice

$$c=21,\qquad\theta=0.11202,\qquad a=0.05665,\qquad s=0.06945.$$

It includes the preprocessing, query, encoding, prime-selection, and instance-construction inequalities, together with

$$2-as/4=1.999016414375,\qquad1.999017-(2-as/4)=0.000000585625>0.$$

Every terminating decimal denotes an exact rational number. The target is the fixed big-$O$ exponent 1.999017; the smaller cutoff is accompanied by residual asymptotic losses in the manuscript and is not asserted as the same fixed bound.

What completing this mission would establish

A complete proof would certify the manuscript's improved integer 3SUM bound in the campaign's common machine model. The gain is an analysis refinement of the inherited algorithm and reductions. It does not claim a new algorithmic framework, optimal parameters, global optimality, or priority over all other work.

The manuscript also gives an auxiliary $O(n^{1.999073})$ bound by retuning the previous estimate. That weaker result is background, not this mission's campaign value. The existing upstream formalization is prior work; it does not automatically certify either refinement. The supplied rational interval verifier checks the parameter inequalities, but those checks alone do not prove a word-RAM running-time theorem. The main goal and the newly drafted supporting statements remain open Lean proof obligations.

Where the difficulty lies

A better tail estimate is insufficient unless every other cost remains within the final budget. Shared encoding work, all queries, deterministic prime selection, witness scanning, and instance construction must be included. The word-size and address bounds must remain valid after changing parameters. Ceiling operations, restricting $D$ to powers of four, and bounded-size exceptions must also be handled.

The central formalization burden is the connection between the analytic estimates and an actual deterministic program. Assuming an oracle with the desired running time would remove that burden and would not establish the stated target. Likewise, checking a finite range of sizes or a floating-point optimizer's output cannot establish the universal algorithmic statement.

Formalization scope and conventions

The environment is Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The foundation reference and the campaign goal's import are retained. Supporting definitions use real logarithms, real powers, natural binomial coefficients, finite sums, and a natural ceiling. Domain hypotheses exclude invalid entropy-tail regimes; endpoint binomial cases are included explicitly.

For $r=1999017/1000000$, the shared time predicate means that there exists $K\in\mathbb N$ such that $T(n)^{1000000}\le K n^{1999017}$ for every $n\ge2$. Correctness and termination still cover every input size, including $n<3$. The manuscript's $\kappa\ge1$ convention must be extended to the campaign's $\kappa=0$ case, and its word-size analysis must justify uniform correctness at every sufficiently large word width. Both are explicit interface obligations.

Reusable contributions include entropy and tail estimates, rigorous logarithm enclosures, and parameterized cost-to-program results. Existing compatible library results should be reused where available. The manuscript and metadata were prepared with AI assistance; this mission makes no claim of completed human review or completed formal verification of the improved bound.

Selected references

• Yuxuan Xu, Deterministic Integer 3SUM in O(n^1.999017) Time via a Sharper Binomial-Tail Analysis, manuscript, 13 October 2026. Author-supplied Hexagon submission page. Target: Theorem 1.1; supporting analysis: Sections 3–6.
• Josh Alman and Virginia Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs, arXiv preprint, 2026. arXiv:2610.06783v1. Inherited ingredients: Section 4, Lemma 29, Theorem 30, Corollary 31, and the deterministic reductions cited in Xu's Section 2.
• Anthropic, Truly Subquadratic 3SUM and Truly Subcubic APSP: a Lean 4 formalization, source repository, 2026. Pinned source at commit e1a4e6508154ea59f030480661590a9fe3018011. Its EndStatement.lean supplies the shared specification, not a proof of this mission's new exponent.

This entry records a deterministic $O(n^{1.962})$ bound for 3SUM on polynomially bounded integers, using the campaign's shared word-RAM model with $O(\log n)$-bit words. Three distinct input positions must sum to zero; repeated values are allowed. The exact exponent is $981/500$.

References

• Source repository: complete Lean proof and verification record

Motivation

The stable matching problem asks for a pairing between two equally sized groups in which no two participants would both rather be matched with each other than with their assigned partners. It was posed and solved by Gale and Shapley in 1962 in the context of college admissions and marriage (Gale–Shapley 1962). Their deferred acceptance algorithm underlies centralized clearinghouses such as the assignment of graduating medical students to hospital residencies, and the theory of stable allocations was recognized by the 2012 Nobel Memorial Prize in Economic Sciences awarded to Shapley and Roth.

Timeline of the results targeted here:

• 1962 — Gale and Shapley: a stable matching always exists, and the men-proposing deferred acceptance algorithm finds one; its outcome is the best stable matching for every man.
• 1971 — McVitie and Wilson: the men-optimal stable matching is simultaneously the worst stable matching for every woman.
• 1981–1982 — Dubins–Freedman and Roth: the men-proposing algorithm is strategy-proof (indeed group strategy-proof) for men, while women can gain by misreporting.
• 1987 — Gusfield (after Knuth and Conway): the stable matchings of an instance form a finite distributive lattice.

Setting

Fix $n \ge 0$. There are $n$ men and $n$ women, both indexed by $\mathrm{Fin}\,n$. Each man $m$ ranks all women strictly: $\mathrm{manRank}_m(w) \in \mathrm{Fin}\,n$ is the position of $w$ in $m$'s list, position $0$ being most preferred; symmetrically each woman $w$ has $\mathrm{womanRank}_w$. Both are bijections. A matching is a bijection $\mu$ from men to women. A pair $(m, w)$ blocks $\mu$ if $\mathrm{manRank}_m(w) < \mathrm{manRank}_m(\mu(m))$ and $\mathrm{womanRank}_w(m) < \mathrm{womanRank}_w(\mu^{-1}(w))$; $\mu$ is stable if no pair blocks it.

The Gale–Shapley algorithm runs in rounds. A state records, for every man, how many women he has proposed to so far, and for every woman, her current provisional fiancé (if any). In each round every unengaged man proposes to the most preferred woman he has not yet proposed to, and every woman keeps the most preferred among her current fiancé and this round's suitors, rejecting the others. The Gale–Shapley outcome is the matching read off from the state after $n^2$ rounds.

Formalization targets

Goal: the algorithm produces a stable matching

$$\forall I,\ \exists \mu,\ \mu \text{ is the Gale–Shapley outcome of } I \ \wedge\ \mu \text{ is stable for } I.$$

This contains termination (all men are engaged after $n^2$ rounds), the fact that the final engagements form a bijection, and stability.

Milestones

1. Termination: after $n^2$ rounds every man is engaged.
2. Existence: every instance has a stable matching.
3. Man-optimality: for the Gale–Shapley outcome $\mu_0$ and every stable $\mu$, $\mathrm{manRank}_m(\mu_0(m)) \le \mathrm{manRank}_m(\mu(m))$ for every man $m$.
4. Woman-pessimality: $\mathrm{womanRank}_w(\mu^{-1}(w)) \le \mathrm{womanRank}_w(\mu_0^{-1}(w))$ for every woman $w$.
5. Truthfulness for men: no single man obtains a strictly better partner (by his true list) by misreporting.
6. Group strategy-proofness for men: no nonempty coalition of men can misreport so that all its members are strictly better off.
7. Weak coalitional manipulation: some coalition can misreport so that some members are strictly better off and the rest keep their partners.
8. Women can manipulate: some woman can obtain a strictly better partner by misreporting.
9. The 3×3 example: the instance $A: YXZ$, $B: ZYX$, $C: XZY$, $X: BAC$, $Y: CBA$, $Z: ACB$ has exactly the three stable matchings $(AY,BZ,CX)$, $(AX,BY,CZ)$, $(AZ,BX,CY)$.
10. Lattice structure: the stable matchings of any instance form a distributive lattice under "every man weakly prefers".

Significance

Existence of stable matchings is the foundation of two-sided matching theory, and the algorithmic proof is constructive. Man-optimality and woman-pessimality show that the proposing side is systematically favored, which is the reason the choice of proposing side matters in practice, as in the 1995 redesign of the residency match. The incentive results (milestones 5–8) explain why participants on the proposing side can safely report their true preferences while the receiving side cannot, and the lattice structure underlies efficient algorithms for enumerating and optimizing over stable matchings.

All results in this mission are classical and proved in the literature. The work here is formalization: a precise model of the round-based algorithm, machine-checked proofs of its correctness and optimality, and the incentive properties, which are usually argued informally.

Difficulty

The goal requires reasoning about an iterated state transformer rather than an abstract existence statement. The step that is usually waved away is the invariant that an unengaged man still has a woman left to propose to, which is what makes the $n^2$ bound and the bijectivity of the final engagements work. Man-optimality needs the invariant that no man is ever rejected by a woman who is his partner in some stable matching, which is not visible from the output alone. Group strategy-proofness is substantially harder than individual truthfulness: the known proofs go through a "blocking lemma" about matchings that are weakly preferred by all men.

Formalization scope

Men and women are Fin n; preferences are strict total orders given as rank bijections Fin n ≃ Fin n; matchings are bijections Fin n ≃ Fin n. The algorithm is the round-based version described in the source: all unengaged men propose simultaneously in each round. The algorithm's output is fixed as the state after exactly $n^2$ rounds; termination within that bound is itself a milestone, so a wrong bound would make the goal false rather than vacuous. The case $n = 0$ is included and is trivial. Incentive results compare Gale–Shapley outcomes of two instances that differ only in the lists of the deviating participants, with gains measured by the deviators' true lists.

The definitions are reusable for further missions on the same article (rural hospitals theorem, hospitals/residents problem). Contributions welcome: invariants of the algorithm, the blocking lemma, and alternative proofs of existence.

Selected references

• D. Gale, L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69(1), 1962, 9–14. https://doi.org/10.2307/2312726
• D. G. McVitie, L. B. Wilson, The stable marriage problem, Communications of the ACM 14(7), 1971, 486–490. https://doi.org/10.1145/362619.362631
• L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley Algorithm, American Mathematical Monthly 88(7), 1981, 485–494. https://doi.org/10.2307/2321753
• A. E. Roth, The Economics of Matching: Stability and Incentives, Mathematics of Operations Research 7(4), 1982, 617–628. https://doi.org/10.1287/moor.7.4.617
• D. Gusfield, Three fast algorithms for four problems in stable marriage, SIAM Journal on Computing 16(1), 1987, 111–128. https://doi.org/10.1137/0216010
• Wikipedia, Stable matching problem. https://en.wikipedia.org/wiki/Stable_matching_problem

Motivation

How large can the order of a single permutation of $n$ objects be? The answer, Landau's function $g(n)$, is a basic invariant of the symmetric group $S_n$: it is the maximum number of times a permutation can be iterated before it returns to the identity. Because the order of a permutation is the least common multiple of its cycle lengths, $g(n)$ is also the largest least common multiple of the parts of a partition of $n$, which ties the question to the distribution of prime numbers.

Timeline.

• 1902–1903. E. Landau proved that $\ln g(n)\sim\sqrt{n\ln n}$.
• 1968. J.-L. Nicolas showed that $g$ is constant on arbitrarily long runs of consecutive integers.
• 1984. J.-P. Massias proved the explicit bound $\ln g(n)\le 1.05313836\sqrt{n\ln n}$ for all $n\ge 1$.
• 1988. Massias, Nicolas and Robin obtained a three-term asymptotic expansion of $\ln g(n)$, its expression through the inverse logarithmic integral, and the equivalence of a one-sided inequality with the Riemann hypothesis.
• 2002. K. Ford's bounds for the Riemann zeta function give the error term $x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$ in the prime number theorem, which can be fed into the 1988 result.

Setting

For a natural number $n$, let $S_n$ be the group of all permutations of an $n$-element set. The order of $\sigma\in S_n$ is the least $k\ge 1$ with $\sigma^k=\mathrm{id}$. Landau's function is

$$g(n)=\max_{\sigma\in S_n}\operatorname{ord}(\sigma).$$

A partition of $n$ is a multiset of positive integers summing to $n$. The prime counting function $\pi(x)$ is the number of primes $p\le x$, the (offset) logarithmic integral is $\mathrm{Li}(x)=\int_2^x\frac{dt}{\ln t}$, and $\mathrm{Li}^{-1}$ is its inverse on $[2,\infty)$. Throughout, $\ln$ is the natural logarithm.

Formalization targets

Goal: Landau's theorem (1902)

$$\lim_{n\to\infty}\frac{\ln g(n)}{\sqrt{n\ln n}}=1.$$

Supporting milestones

1. Partition characterization: $g(n)=\max\{\operatorname{lcm}(\lambda):\lambda\vdash n\}$.
2. Initial values $g(0),\dots,g(8)=1,1,2,3,4,6,6,12,15$.
3. Nicolas (1968): for every $m$ there is $n$ with $g(n)=g(n+1)=\dots=g(n+m)$.
4. Massias–Nicolas–Robin (1988): $\ln g(n)=\sqrt{n\ln n}\Bigl(1+\frac{\ln\ln n-1}{2\ln n}-\frac{(\ln\ln n)^2-6\ln\ln n+9}{8(\ln n)^2}+O\bigl((\tfrac{\ln\ln n}{\ln n})^3\bigr)\Bigr)$.
5. Ford (2002): $\pi(x)-\mathrm{Li}(x)=O\bigl(x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})\bigr)$ for some $c>0$.
6. Massias–Nicolas–Robin (1988): if $\pi(x)-\mathrm{Li}(x)=O(R(x))$ with $R(x)=x\exp(-c(\ln x)^{3/5}(\ln\ln x)^{-1/5})$, then $\ln g(n)=\sqrt{\mathrm{Li}^{-1}(n)}+O\bigl(R(\sqrt{n\ln n})\ln n\bigr)$.
7. Riemann hypothesis criterion: $\ln g(n)<\sqrt{\mathrm{Li}^{-1}(n)}$ for all large $n$ $\iff$ RH.
8. $g(n)\le e^{n/e}$ for all $n$, with equality only at $n=0$.
9. Massias (1984): $g(n)\le\exp(1.05314\sqrt{n\ln n})$.

Significance

Landau's theorem pins down the growth rate of the largest element order in $S_n$, which bounds, for example, how long any fixed shuffle of $n$ cards can be repeated before the deck returns to its starting order. The refined statements quantify the second-order behaviour and connect it to the error term in the prime number theorem; the criterion in milestone 7 is one of the known elementary reformulations of the Riemann hypothesis, and is included as a faithful statement of the source, not as an expected deliverable. The other results are proved in the literature; formalizing them requires building the partition/lcm description of element orders in $S_n$ and quantitative prime-counting estimates on top of Mathlib.

Difficulty

The order of a permutation is easy to compute from its cycle type, but maximizing an lcm over all partitions is a non-linear optimization: the optimum uses prime powers whose sizes are dictated by the distribution of primes, so even the leading-order asymptotics need Chebyshev-type or prime number theorem estimates, and the refined milestones need the prime number theorem with an explicit error term.

Formalization scope

• $S_n$ is Equiv.Perm (Fin n); $g(n)$ is the supremum of orderOf σ over the finite group (a natural number; $g(0)=1$).
• Partitions are Mathlib's Nat.Partition n; the lcm of a partition is the Multiset.lcm of its parts.
• Real logarithms use Real.log (which returns $0$ at $0$ and is defined for negative input); all asymptotic statements are about $n\to\infty$, so the values at small $n$ are irrelevant there. The bounds in milestones 8–9 are stated for every $n$ and are true at $n=0,1$.
• $\pi(x)$ for real $x$ is Nat.primeCounting ⌊x⌋₊; $\mathrm{Li}$ is the offset logarithmic integral $\int_2^x dt/\ln t$; $\mathrm{Li}^{-1}(y)$ is the least $x\ge2$ with $\mathrm{Li}(x)\ge y$, which for $y\ge0$ is the inverse function value. Replacing $\mathrm{Li}$ by the full integral $\mathrm{li}$ changes the inverse by $O(\ln n)$ and does not affect any of the asymptotic statements.
• The Riemann hypothesis is Mathlib's RiemannHypothesis.

Contributions of reusable infrastructure (cycle-type lcm, prime-counting error terms, the logarithmic integral) are welcome.

Selected references

• E. Landau, Über die Maximalordnung der Permutationen gegebenen Grades, Arch. Math. Phys. Ser. 3, vol. 5, 1903.
• J.-L. Nicolas, Sur l'ordre maximum d'un élément dans le groupe $S_n$ des permutations, Acta Arithmetica 14 (1968), 315–332.
• J.-P. Massias, Majoration explicite de l'ordre maximum d'un élément du groupe symétrique, Ann. Fac. Sci. Toulouse Math. (5) 6 (1984), 269–281.
• J.-P. Massias, J.-L. Nicolas, G. Robin, Évaluation asymptotique de l'ordre maximum d'un élément du groupe symétrique, Acta Arithmetica 50 (1988), 221–242.
• K. Ford, Vinogradov's integral and bounds for the Riemann zeta function, Proc. London Math. Soc. 85 (2002), 565–633. https://doi.org/10.1112/S0024611502013655
• W. Miller, The maximum order of an element of a finite symmetric group, Amer. Math. Monthly 94 (1987), 497–506.
• OEIS A000793. https://oeis.org/A000793

Motivation

The spectral radius of a graph, the largest eigenvalue of its adjacency matrix, measures how densely and how unevenly the edges of the graph are distributed. Asking which graph in a class maximizes it is a spectral analogue of the extremal question "which graph in the class has the most edges". For planar graphs the question has a long history in spectral graph theory, going back at least to Schwenk and Wilson. It also arose in geography, where the spectral radius serves as a measure of the connectivity of planar networks. To compare real networks with a theoretical upper bound, geographers wanted the planar graph of maximum spectral radius (arXiv:1606.01916v2, p. 3).

Timeline, as recorded by Tait and Tobin (pp. 1–3):

• 1978, Schwenk and Wilson: early study of the eigenvalues of planar graphs.
• 1991, Boots and Royle, and independently 1993, Cao and Vince: conjecture that the planar graph on $n \ge 9$ vertices of maximum spectral radius is $P_2 + P_{n-2}$ (Conjecture 1 of the paper). The conjecture is false for $n \in \{7, 8\}$, so some lower bound on $n$ is necessary (p. 2).
• 1988–2000: successive improvements of the upper bound on the spectral radius of planar graphs, by Hong (1988, 1995, 1998), Cao and Vince (1993), Guiduli (1996) and Ellingham and Zha (2000). These bounds do not identify the extremal graph.
• 2010, Dvořák and Mohar: an upper bound on the spectral radius of planar graphs of given maximum degree.
• Guiduli and Hayes were reported by Ellingham and Zha to have proved the conjecture for large $n$. The preprint never appeared (p. 3).
• 2017, Tait and Tobin: proof of the conjecture for all sufficiently large $n$ (Theorem 15).

Setting

All graphs are finite and simple. A graph on $n$ vertices has vertex set $\{0, 1, \dots, n-1\}$. Its adjacency matrix $A(G)$ is the $n \times n$ real matrix with entry $1$ in position $(u, w)$ when $u \sim w$ and $0$ otherwise. Its eigenvalues are real, and the largest is the spectral radius $\lambda_1(G)$.

A graph is planar if it can be drawn in the plane with vertices as distinct points and edges as simple arcs joining their ends, such that an arc meets no vertex other than its ends and two arcs meet only at common ends.

For graphs $G$ and $H$ on disjoint vertex sets, the join $G + H$ is the graph on the union of the two vertex sets that keeps every edge of $G$ and of $H$ and adds every edge between a vertex of $G$ and a vertex of $H$. Write $K_2$ for a single edge, $P_m$ for the path on $m$ vertices, and $K_2 + P_{n-2}$ for their join: two adjacent vertices, both joined to every vertex of a path on the remaining $n - 2$ vertices. The paper also writes it $P_2 + P_{n-2}$.

A planar graph $G$ on $n$ vertices is a planar spectral maximizer if $\lambda_1(G') \le \lambda_1(G)$ for every planar graph $G'$ on the same $n$ vertices.

The milestones refer to a leading eigenvector $\mathbf v$ of a maximizer, scaled so that every entry is positive and the largest entry is $1$, and to a vertex $x$ with $\mathbf v_x = 1$. For a parameter $\varepsilon > 0$ they use the sets $L = \{z : \mathbf v_z > \varepsilon\}$ and $S = V(G) \setminus L$, the edge counts $e(X)$ (edges inside $X$) and $e(X, Y)$ (edges between $X$ and $Y$), and a second vertex $w$ with $\mathbf v_w > 1 - 24\varepsilon$ that is adjacent to all but $94\varepsilon n$ vertices of $S$.

Formalization targets

Goal: Theorem 15

$$\exists N_0\ \forall n \ge N_0\ \forall G \text{ on } n \text{ vertices}: \quad G \text{ is a planar spectral maximizer} \iff G \cong K_2 + P_{n-2}.$$

The threshold $N_0$ is not fixed. The paper proves the statement only for $n$ beyond an unspecified bound, and the conjecture's bound $n \ge 9$ remains open. The equivalence encodes "the unique maximizer is $K_2 + P_{n-2}$": every maximizer is isomorphic to it, and it is itself a maximizer.

Milestones, in the order of the proof

1. If $H$ is a proper spanning subgraph of a connected graph $G$, then $\lambda_1(H) < \lambda_1(G)$ (§1.2, already proved on the platform).
2. A planar graph on $n \ge 3$ vertices has no $K_{3,3}$ subgraph and at most $3n - 6$ edges, and each of its bipartite subgraphs has at most $2n - 4$ edges (p. 8).
3. Lemma 8: $\sqrt{2n-4} < \lambda_1 < \sqrt{6n}$.
4. The counts $|L| \le 3\sqrt{2n-4}/\varepsilon$, $e(S, L) \le 2n - 4$, $e(S) \le 3n - 6$, $e(L) \le 9\sqrt{2n-4}/\varepsilon$ (p. 8).
5. Lemma 9: $\sum_{z \in L} \mathbf v_z \le \varepsilon\sqrt{2n-4} + 18/\varepsilon$ and $\sum_{z \in S} \mathbf v_z \le (1 + 3\varepsilon)\sqrt{2n-4}$.
6. Eq. (7): $\sum_{y \sim u,\, y \in S} \mathbf v_y \ge (\mathbf v_u - \varepsilon)\sqrt{2n-4} - 18/\varepsilon$ for $u \in L$.
7. Lemma 10: $\mathbf v_z > 1/\sqrt{6n}$ for every vertex $z$.
8. $|\{y \in S : y \not\sim x\}| \le 14\varepsilon n$ (p. 10).
9. Lemma 11: a vertex $w \in L$, $w \ne x$, with $\mathbf v_w > 1 - 24\varepsilon$ and $|\{y \in S : y \not\sim w\}| \le 94\varepsilon n$.
10. Lemma 12: $\mathbf v_u < 1/10$ for every $u \notin \{x, w\}$.
11. Lemma 13: $x \sim w$.
12. Lemma 14: every vertex other than $x$ and $w$ is adjacent to both.
13. A planar graph with two distinct vertices adjacent to all other vertices is a spanning subgraph of $K_2 + P_{n-2}$ (proof of Theorem 15, p. 13).

Significance

The result. Theorem 15 settles the Boots–Royle / Cao–Vince conjecture for all large $n$. It identifies the planar graph of maximum spectral radius exactly, so the theoretical upper bound that the geographic application asks for is $\lambda_1(K_2 + P_{n-2})$. Along the way, Lemmas 8–14 describe the eigenvector of the extremal graph: two vertices carry almost all of the eigenvector weight, and every other entry is below $1/10$. The same method proves the outerplanar analogue (Theorem 7, the companion mission of this series).

Formalizing it. The theorem is proved on paper and has no machine-checked proof. Formalizing it needs several pieces that are absent from Mathlib or the platform and are reusable: the edge bound $3n - 6$ and the bipartite bound $2n - 4$ for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$ and of their subdivisions, Rayleigh-quotient comparison of spectral radii, and the face structure of maximal planar graphs. Each milestone is a self-contained target.

Difficulty

Counting edges does not separate the candidates. A maximizer can be taken to be a maximal planar graph, so it has exactly $3n - 6$ edges. Every maximal planar graph on $n$ vertices has the same number of edges, and the standard lower bound $\lambda_1 \ge 2|E|/n$ is the same for all of them. The extremal graph is pinned down only through its eigenvector. One has to show that the weight concentrates on two vertices, which are then forced to be adjacent to each other (Lemma 13) and to every other vertex (Lemma 14). Lemma 13 is the step specific to planarity. It uses the triangular faces of a maximal planar graph to find an edge switch that keeps the graph planar. In the formal setting, planarity is topological, so every planarity fact of the argument (the edge counts, the $K_{3,3}$ and $K_5$ obstructions, the faces of a triangulation) has to be derived from the drawing.

Formalization scope

• Graphs are SimpleGraph (Fin n). "$G$ is $K_2 + P_{n-2}$" is a graph isomorphism G ≃g bookPath n, where bookPath n lives on Fin 2 ⊕ Fin (n - 2). It is not an equality on a fixed labelling.
• $\lambda_1$ is the published WangKangXue.SpectralTuran.specRad, the largest eigenvalue of the real adjacency matrix.
• Planarity is the published topological RobertsonSeymour1986.GM5.IsPlanar: a drawing by simple arcs. It is not replaced by $K_5$/$K_{3,3}$-minor-freeness or by an edge count, either of which would change the class the maximum ranges over.
• Extremality is IsSpecMax IsPlanar G: $G$ is planar and $\lambda_1(G') \le \lambda_1(G)$ for every planar $G'$ on Fin n. Every milestone from Lemma 8 to Lemma 14 assumes it. These lemmas are false for an arbitrary planar graph, so a statement that drops the hypothesis, or replaces it by a property implying the conclusion, is not acceptable.
• The eigenvector is universally quantified: every $\mathbf v$ with $A\mathbf v = \lambda_1 \mathbf v$, all entries positive, all entries at most $1$, and every $x$ with $\mathbf v_x = 1$. Such a vector exists because the maximizer is connected (Perron–Frobenius). A statement that only asserts the existence of some eigenvector is weaker and is ruled out.
• Quantifiers. "For $n$ sufficiently large" is $\exists N\ \forall n \ge N$, and $N$ may depend on $\varepsilon$. Milestones 4–8 hold for every $\varepsilon > 0$. Lemmas 11–14 hold for $0 < \varepsilon < \varepsilon_0$ with an unspecified $\varepsilon_0$, because the paper chooses $\varepsilon$ small. The quantifier on $\varepsilon$ is always outermost, so $\varepsilon$ never depends on $n$ or $G$. Lemmas 12–14 hold for every vertex $w$ satisfying the conclusion of Lemma 11 (the predicate IsSecondHub), with the constants $24$ and $94$.
• Added hypotheses. $n \ge 3$ in the planar facts and in Lemma 8, where the paper's standing "$n$ large enough" is needed only to that extent. The page names the vertex of Lemma 12 $v$, the same letter as the eigenvector; it is renamed $u$. Lemma 14's set $A$ is stated in unfolded form.
• Infrastructure that a complete development needs: Euler's formula for topologically planar graphs, the non-planarity of $K_{3,3}$ and $K_5$, Perron–Frobenius for connected graphs, and the Rayleigh quotient. Proofs of the planar facts (milestone 2) are reusable well beyond this mission. Contributions toward any of them are welcome.

Selected references

• M. Tait and J. Tobin, Three conjectures in extremal spectral graph theory, J. Combin. Theory Ser. B (2017). Preprint arXiv:1606.01916v2. https://arxiv.org/abs/1606.01916, DOI https://doi.org/10.1016/j.jctb.2017.04.006
• B. N. Boots and G. F. Royle, A conjecture on the maximum value of the principal eigenvalue of a planar graph, Geographical Analysis 23(3) (1991), 276–282.
• D. Cao and A. Vince, The spectral radius of a planar graph, Linear Algebra Appl. 187 (1993), 251–257.
• A. J. Schwenk and R. J. Wilson, On the eigenvalues of a graph, in: Selected Topics in Graph Theory, Academic Press, 1978, 307–336.
• Hong Yuan, A bound on the spectral radius of graphs, Linear Algebra Appl. 108 (1988), 135–139.
• M. N. Ellingham and X. Zha, The spectral radius of graphs on surfaces, J. Combin. Theory Ser. B 78(1) (2000), 45–56.
• Z. Dvořák and B. Mohar, Spectral radius of finite and infinite planar graphs and of graphs of bounded genus, J. Combin. Theory Ser. B 100(6) (2010), 729–739.

Bibliographic data as given in the bibliography of Tait and Tobin (pp. 21–23).