The OR Formalization Drive

Motivation

Set cover is one of the basic covering problems of combinatorial optimization: given a ground set and a family of subsets with costs, choose a cheapest subfamily whose union contains every element. In many applications the elements to be covered are not known in advance but appear over time: requests for a service that must be served by opening facilities, clients that must be assigned to servers, or constraints of a covering program that are revealed one at a time. Each arriving element must be covered at once, and decisions cannot be undone. This is the online set cover problem, introduced by Alon, Awerbuch, Azar, Buchbinder and Naor (SIAM J. Comput. 39(2), 2009; conference version STOC 2003).

The quality of an online algorithm is measured by its competitive ratio: the worst case, over all arrival sequences, of the ratio between the algorithm's cost and the cost of an optimal offline cover of the elements that actually arrived. The paper gives a deterministic algorithm with ratio $O(\log m \log n)$, where $n$ is the number of elements and $m$ the number of sets, and shows a nearly matching lower bound for deterministic algorithms. Its algorithm for the weighted case, analysed with a potential function, became a template for the online primal–dual method surveyed by Buchbinder and Naor (Found. Trends Theor. Comput. Sci. 3(2–3), 2009).

This mission formalizes the core of the weighted result: the algorithm that is given a value $\alpha$ at least the optimal cost, and its guarantee (Theorem 3.4).

Setting

The ground set $X$ has $n = |X|$ elements and the family $\mathcal S$ has $m = |\mathcal S|$ sets; every set $S$ has a cost $c_S > 0$. Both are known to the algorithm in advance. For an element $j$, $\mathcal S_j$ denotes the sets containing $j$. Elements of an unknown subset of $X$ arrive one at a time in a sequence $\sigma$; on arrival each must be covered by a chosen set. The chosen family $\mathcal C$ can only grow. $\mathcal C_{OPT}$ is any family covering every arriving element, and $c(\mathcal C_{OPT}) = \sum_{S \in \mathcal C_{OPT}} c_S$.

The algorithm is given $\alpha \ge c(\mathcal C_{OPT})$. It discards sets costing more than $\alpha$, buys sets costing at most $\alpha/m$ outright, and rescales costs; on the resulting normalized instance $1 \le c_S \le m$ and $c_S \le \alpha$ for every set (p. 365).

The algorithm keeps a weight $w_S > 0$ for every set, initially $w_S = 1/m^2$; the weight of an element is $w_j = \sum_{S \in \mathcal S_j} w_S$. With $C$ the set of covered elements and $\chi_{\mathcal C}$ the indicator of $\mathcal C$, the potential is

$$\Phi = \sum_{j \notin C} n^{2 w_j} + n \cdot \exp\Big(\frac{1}{2\alpha} \sum_{S \in \mathcal S} \big(c_S \chi_{\mathcal C}(S) - 3 w_S c_S \log n\big)\Big),$$

with natural logarithms throughout. When $j$ arrives with $w_j \ge 1$ nothing happens; otherwise the algorithm performs weight augmentation steps while $w_j < 1$. In a step, for each $S \in \mathcal S_j$: (a) $w_S \leftarrow w_S (1 + \frac{1}{n c_S})$; (b) if $S \notin \mathcal C$, add $S$ to $\mathcal C$ when $\Phi$ does not exceed its value before (a); (c) if $\Phi$ has increased, return FAIL.

In Lean, the instance is the published OnlinePrimalDual.OnlineSetCover.SetCoverInstance over finite types X (elements) and T (sets), with the published elementWeight, coveredBy and potential. The run is OnlineSetCover.Weighted.Reachable inst α σ, the set of configurations reachable from initState σ under the transition relation Step.

Formalization targets

Goal: Theorem 3.4

On the normalized instance, with $\mathcal C_{OPT}$ covering $\sigma$, $c(\mathcal C_{OPT}) \le \alpha$, and $n \cdot n^{2/m} + n < n^2$, every reachable configuration is a running state (never FAIL) in which (i) every $j \in X$ with $w_j \ge 1$ is covered, and (ii)

$$\sum_{S \in \mathcal C} c_S \le 3 \log n \Big(1 + \Big(1 + \frac1n\Big)\alpha \log\Big(m^2\Big(1+\frac1n\Big)\Big)\Big) + 2\alpha \log n = (6 + o(1))\,\alpha \log m \log n.$$

Milestones

• Lemma 3.1 (p. 365): the number $N$ of augmentation steps satisfies $N \le \sum_{S \in \mathcal C_{OPT}} (n c_S + 1)\log(m^2(1 + 1/n)) \le (n+1)\alpha\log(m^2(1+1/n))$.
• Lemma 3.2 (p. 366): throughout, $\sum_S w_S c_S \le 1 + N/n \le 1 + (1 + 1/n)\alpha\log(m^2(1+1/n))$.
• Lemma 3.3 (p. 366): a per-set step with $c_S \le \alpha$ never increases $\Phi$; in particular the algorithm never fails.

The Proved platform theorem OnlinePrimalDual.OnlineSetCover.algorithm_correctness (the last paragraph of the proof of Theorem 3.4, with the invariant $\Phi < n^2$ assumed) is included as a supporting reference.

Significance

Theorem 3.4 is the analysis of the subroutine; with the doubling over guesses of $\alpha$ described on pp. 364–365 (which loses a factor of at most 4) it yields the paper's deterministic $O(\log m \log n)$-competitive algorithm for weighted online set cover. The lower bound of Section 4 shows that no deterministic algorithm can do much better on general instances, so the result is close to the deterministic optimum. The technique, a potential that couples a fractional multiplicative-weights solution to a deterministic rounding, reappears in online covering and packing, online facility location and related problems.

The result is proved in the paper and restated in the Buchbinder–Naor monograph. On Prove2Me, the monograph's final step (from the invariant $\Phi < n^2$ to the cost bound) is a Proved theorem, and its expectation form of the monotonicity lemma is Disproved because it omits the hypothesis $c_S \le \alpha$. Neither the full statement about the algorithm's run nor Lemmas 3.1, 3.2 and the corrected Lemma 3.3 are formalized on the platform. This mission produces them, with the $o(1)$ terms replaced by explicit expressions.

Difficulty

The cost bound in the last step is short once two facts about the run are available: that $\Phi$ stays below $n^2$, and that the fractional cost $\sum_S w_S c_S$ stays logarithmic. Neither is a local fact about one state. The first requires showing that, at every per-set step, one of the two deterministic choices (add $S$ or not) does not increase $\Phi$; the paper proves this by a probabilistic argument over an auxiliary randomized choice, and the bound on the exponential term depends on the cost of the set being at most $\alpha$. The platform's earlier statement of this lemma, which omits that hypothesis, is Disproved. The second requires a bound on the number of augmentation steps over the whole run, which depends on the run's history and not on any single state. In Lean both are inductions over an operational semantics with real-valued exponentials and powers $n^{2 w_j}$, where the initial bound $\Phi < n^2$ is a genuine size condition on $n$ and $m$.

Formalization scope

The run is a small-step transition relation. A state records the weights, the cover, the number of augmentation steps begun, the elements not yet given, and the position inside the current step; FAIL is a separate terminal configuration. The order in which a step visits $\mathcal S_j$ is arbitrary and may differ between steps; every statement holds for every order. "Throughout the algorithm" means every reachable configuration, including those between per-set substeps. Arrival sequences are arbitrary lists (repetitions allowed) of elements covered by $\mathcal C_{OPT}$.

Conventions: costs, weights and $\alpha$ are real; $n$ and $m$ are the cardinalities of the finite types cast to $\mathbb R$; $\log$ is Real.log; $n^{2 w_j}$ and $n^{2/m}$ are real powers. The paper's asymptotic expressions are replaced by what its proofs establish:

• Lemma 3.1: $(2 + o(1)) n\alpha\log m$ becomes $(n+1)\alpha\log(m^2(1+1/n))$;
• Lemma 3.2: $(2 + o(1))\alpha\log m$ becomes $1 + (1+1/n)\alpha\log(m^2(1+1/n))$, together with the intermediate bound $1 + N/n$;
• Theorem 3.4 (ii): $(6 + o(1))\alpha\log m\log n$ becomes $3\log n\,(1 + (1+1/n)\alpha\log(m^2(1+1/n))) + 2\alpha\log n$;
• "n and m large" becomes the hypothesis $n \cdot n^{2/m} + n < n^2$ used for the initial potential (it holds, for instance, when $n \ge 4$ and $m \ge 3$).

The goal is a statement about the configurations the algorithm actually reaches from $w_S = 1/m^2$ and the empty cover. Taking the invariant $\Phi < n^2$ or the fractional-cost bound as a hypothesis on an arbitrary state would trivialize it, and is ruled out: those are exactly what the milestones establish. The doubling wrapper for unknown $\alpha$ is not part of this mission.

A complete development needs an invariant for reachable states (positive weights, steps of an element processed in full), the per-set potential inequality, and the step-counting argument. The per-set inequality is reusable for the monograph's version of the algorithm. Contributions of proofs of any milestone, and of auxiliary invariants as separate lemmas, are welcome.

Selected references

• N. Alon, B. Awerbuch, Y. Azar, N. Buchbinder, J. Naor, The Online Set Cover Problem, SIAM Journal on Computing 39(2):361–370, 2009. https://doi.org/10.1137/060661946
• N. Buchbinder, J. Naor, The Design of Competitive Online Algorithms via a Primal–Dual Approach, Foundations and Trends in Theoretical Computer Science 3(2–3):93–263, 2009. https://doi.org/10.1561/0400000024

Motivation

When many self-interested users share resources whose cost grows with use (links of a network, servers, machines), each user picks the option that is cheapest for them given what the others do, and the resulting equilibrium can be worse for the group than a centrally planned allocation. The price of anarchy, introduced by Koutsoupias and Papadimitriou (STACS 1999), measures this loss as the worst ratio between the social cost of an equilibrium and the optimal social cost. Congestion games (Rosenthal 1973) are the standard finite model of such resource sharing: they always have pure Nash equilibria, and they cover atomic routing, load balancing and many network design questions.

Timeline of the linear-latency case:

• 2002: Roughgarden and Tardos (J. ACM) bound the price of anarchy of nonatomic selfish routing with linear latencies by $4/3$.
• 2005: Awerbuch, Azar and Epstein (STOC 2005) and, independently, Christodoulou and Koutsoupias (STOC 2005) show that for atomic (finite) congestion games with linear latencies the pure price of anarchy of the total cost is $5/2$. Awerbuch, Azar and Epstein also obtain $(3+\sqrt5)/2 \approx 2.618$ for weighted players.
• 2005: Christodoulou and Koutsoupias observe that their argument for $5/2$ extends to mixed Nash equilibria, at the price of the larger constant $(3+\sqrt5)/2$ (their Theorem 14, the goal of this mission).

Setting

A congestion game consists of a finite set $N$ of players, a finite set $E$ of facilities, for each player $i$ a collection $\Sigma_i$ of pure strategies, each a subset of $E$, and for each facility $e$ a latency function $f_e : \mathbb N \to \mathbb R$. In a pure profile $A = (A_1, \dots, A_n)$, $A_i \in \Sigma_i$, the load $n_e(A)$ is the number of players whose set contains $e$, and player $i$ pays

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

The social cost of a pure profile is $\mathrm{SUM}(A) = \sum_{i\in N} c_i(A)$ ($N$ times the average cost). Latencies are linear: $f_e(k) = a_e k + b_e$ with $a_e, b_e \ge 0$.

A mixed strategy $p_i$ of player $i$ is a probability distribution on $\Sigma_i$. The players randomize independently, so the pure profile $s$ occurs with probability $\Pr(s) = \prod_j p_j(s_j)$. Player $i$'s expected cost is $\mathbb E[c_i] = \sum_s \Pr(s)\, c_i(s)$, and the expected load of $e$ is $\mathbb E[n_e] = \sum_s \Pr(s)\, n_e(s)$. A mixed profile is a mixed Nash equilibrium if no player can lower their expected cost by switching unilaterally to another distribution on their strategies. The social cost of a mixed profile is the sum of the expected costs, $\mathrm{SUM}(p) = \sum_i \mathbb E[c_i]$.

In Lean: CongestionGame ι E with fields strategies and latency, load, cost, IsProfile, sumCost, IsLinear, expCost, expLoad, mixedSumCost and IsMixedNash, all in the namespace CongestionPoA.Mixed; lotteries and independent randomization come from the platform definition agt_games (AGT.IsLottery, AGT.profileProb, AGT.IsMixedNash).

Formalization targets

Goal: Theorem 14

For every congestion game with linear latencies, every mixed Nash equilibrium $p$ and every pure profile $P$ with $P_i \in \Sigma_i$,

$$\sum_{i\in N} \mathbb E[c_i] \;\le\; \frac{3+\sqrt5}{2}\,\mathrm{SUM}(P).$$

Taking $P$ optimal, the mixed price of anarchy of the average social cost is at most $(3+\sqrt5)/2$.

Milestones

1. Lemma 3 (corrected). For real $x \ge 0$ and integer $y \ge 0$, $y(x+1) \le \frac{\sqrt5-1}{4}x^2 + \frac{\sqrt5+5}{4}y^2$.
2. Deviation inequality (Theorem 1's proof, mixed). At a mixed Nash equilibrium, for every player $i$,

$$\mathbb E[c_i] \le \sum_{e\in P_i}\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

3. Summing step (Theorem 1's proof, mixed).

$$\sum_i \mathbb E[c_i] \le \sum_{e\in E} n_e(P)\bigl(a_e(\mathbb E[n_e]+1) + b_e\bigr).$$

Significance

The bound says that randomization by the players cannot make linear congestion games much worse than pure play: the loss stays within a constant factor independent of the number of players and facilities. Mixed equilibria matter because they always exist in every finite game and because they model populations of users whose individual choices are not known in advance. The same authors report (PDF p. 2) extending these bounds to correlated equilibria with the same values, which places the mixed bound in a hierarchy of equilibrium notions whose worst cases coincide.

The result is proved in the paper, in one sentence that defers to the proof of Theorem 1. The work here is a complete machine-checked version: the expected-cost layer for congestion games on top of agt_games, the deviation and summing inequalities under product distributions, and the corrected Lemma 3. The paper prints Lemma 3 for all nonnegative reals $x, y$, where it is false (at $x = 0$, $y = 1/10$ the left side is $0.1$ and the right side about $0.018$); the formal statement keeps $y$ an integer, which is how the lemma is used. No formalization of congestion-game price-of-anarchy bounds was on the platform when this mission was drafted.

Difficulty

The pure proof compares $n_e(P)(n_e(A)+1)$ with $n_e(A)^2$ and $n_e(P)^2$ through an integer inequality (Lemma 1). Under a mixed equilibrium the equilibrium side is an expectation, so the cost of a facility is no longer a function of one integer load, and Lemma 1's constant $1/3$ is not available for real arguments: a real-variable version is needed, and the constant degrades from $5/2$ to $(3+\sqrt5)/2$. A second obstacle is bookkeeping: the deviating player's load changes only on their own deviation, while the other players' randomization stays independent, and the expected cost of a player has to be related to expected facility loads, which uses linearity of the latencies in an essential way. The naive idea of applying Theorem 1 to each pure profile in the support of the equilibrium fails, because those profiles are not themselves Nash equilibria.

Formalization scope

Players and facilities are finite types ι and E; profiles are functions ι → Finset E, with feasibility IsProfile a separate predicate. Latencies are real-valued on natural-number loads, and "linear" means affine with nonnegative coefficients, $f_e(k) = a_e k + b_e$; the paper displays only the identity latency $f_e(k)=k$ and states that its proofs extend. Mixed strategies are real weight functions on the finite strategy type $\Sigma_i$; independence is built into AGT.profileProb; Nash deviations range over all lotteries, which is equivalent to pure deviations. agt_games maximizes payoffs, so the game is passed to it with payoff $-c_i$. The goal is stated against every feasible pure profile rather than as a ratio, so no division by an optimum that may be $0$ occurs. The social cost is the expected sum of the players' costs; the paper's second option, $\sum_e \mathbb E[n_e^2]$, is not part of this mission. A version with correlated distributions on profiles, or one that bounds the cost of an "averaged" profile instead of the expected cost, is a different statement and does not discharge the goal.

A complete development needs elementary finite-sum manipulation of product distributions (marginals of AGT.profileProb, expectations of loads), and a Jensen-type inequality $(\mathbb E[n_e])^2 \le \mathbb E[n_e^2]$ for finite distributions. The expectation lemmas for congestion games are reusable for the other mixed results of the literature (weighted games, polynomial latencies). Proofs of the milestones, of the expectation layer, and alternative arguments are all welcome.

Selected references

• G. Christodoulou, E. Koutsoupias, The Price of Anarchy of Finite Congestion Games, STOC 2005, pp. 67–73. https://doi.org/10.1145/1060590.1060600
• B. Awerbuch, Y. Azar, A. Epstein, The Price of Routing Unsplittable Flow, STOC 2005, pp. 57–66. https://doi.org/10.1145/1060590.1060599
• E. Koutsoupias, C. Papadimitriou, Worst-case Equilibria, STACS 1999, LNCS 1563, pp. 404–413. https://doi.org/10.1007/3-540-49116-3_38
• R. W. Rosenthal, A Class of Games Possessing Pure-Strategy Nash Equilibria, International Journal of Game Theory 2 (1973), pp. 65–67. https://doi.org/10.1007/BF01737559
• T. Roughgarden, É. Tardos, How Bad Is Selfish Routing?, Journal of the ACM 49 (2002), pp. 236–259. https://doi.org/10.1145/506147.506153

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

A finite Markov decision problem with discounting is solved by Howard's policy improvement routine: start from a stationary policy, switch to actions that do better against its value, repeat. When the discount factor $\beta$ tends to $1$ the total discounted income typically diverges, and the natural targets become the long-run average income and, among policies with the best average, the policy that does best in the transient phase. Howard treated this undiscounted case directly (Howard, 1960). David Blackwell's 1962 paper (Blackwell, 1962) treats $\beta = 1$ as a limit of $\beta < 1$: it expands the discounted return of a stationary policy in powers of $1-\beta$ and reads off which policies remain good as $\beta \to 1$. The two leading coefficients of that expansion, the gain $x(f)$ and the bias $y(f)$, became the standard objects of average-reward and sensitive-discount optimality (Veinott, 1969; Puterman, 1994, Ch. 8–10).

Timeline. Howard (1960) gives policy iteration for discounted and average-income problems. Blackwell (1962) proves that some stationary policy is optimal for all $\beta$ near $1$ (his Theorem 5, the subject of a companion mission) and, in Theorem 4, characterizes the nearly optimal stationary policies through $x$ and $y$. Miller and Veinott (1969) and Veinott (1969) extend the expansion to all orders ($n$-discount optimality).

Setting

There are finitely many states $s \in S$ and a finite nonempty set $A$ of actions. Action $a$ in state $s$ pays an income $i(s,a) \in \mathbb R$ and moves the system to $s'$ with probability $q(s' \mid s,a)$. $F$ is the finite set of decision rules $f : S \to A$. A policy is a sequence $\pi = \{f_1, f_2, \dots\}$ of decision rules; $f^{(\infty)}$ uses $f$ every day, and $(g, \pi)$ uses $g$ first and then $\pi$. For $f \in F$, $r(f)$ is the vector $(i(s,f(s)))_s$ and $Q(f)$ the Markov matrix $(q(s' \mid s,f(s)))_{s,s'}$. The discounted return of $\pi$ is the vector

$$V_\beta(\pi) = \sum_{n=0}^\infty \beta^n Q(f_1)\cdots Q(f_n)\, r(f_{n+1}), \qquad 0 \le \beta < 1,$$

and $V_\beta(f)$ abbreviates $V_\beta(f^{(\infty)})$. Vectors are compared coordinatewise; $w_1 > w_2$ means $w_1 \ge w_2$ and $w_1 \neq w_2$. A policy is β-optimal if its return dominates that of every policy, and $U(\beta)$ is the return of a β-optimal policy. It is optimal if it is β-optimal for all $\beta$ sufficiently near $1$, and nearly optimal if $U(\beta) - V_\beta(\pi) \to 0$ as $\beta \to 1$.

For any Markov matrix $Q$, the limit matrix $Q^*$ is the limit of $(I + Q + \cdots + Q^N)/(N+1)$, and the deviation matrix is $H = (I - Q + Q^*)^{-1} - Q^*$. For a rule $f$, $Q^*(f)$ and $H(f)$ are those of $Q(f)$, and

$$x(f) = Q^*(f)\, r(f), \qquad y(f) = H(f)\, r(f).$$

With $p(s,a)w = \sum_{s'} q(s' \mid s,a) w_{s'}$, the set $G(s,f)$ consists of the actions $a$ with $p(s,a)x(f) > x_s(f)$, or with $p(s,a)x(f) = x_s(f)$ and $i(s,a) + p(s,a)y(f) > x_s(f) + y_s(f)$; $E(s,f)$ consists of those with equality in both.

Formalization targets

Goal: Theorem 4(e)

For any $f_0$ with $G(s,f_0) = \varnothing$ for all $s$:

$$x(f_0) \ge x(g)\ \ \forall g \in F;\qquad \exists f^* \in F^* := \{g : x(g) = x(f_0)\}\ \text{with}\ y(f^*) \ge y(g)\ \forall g \in F^*;$$ $$g^{(\infty)} \text{ is nearly optimal} \iff x(g) = x(f^*) \text{ and } y(g) = y(f^*).$$

Milestones and intermediate results

Milestones: Lemma 1(b) ($\operatorname{rank}(I-Q) + \operatorname{rank} Q^* = S$), Theorem 4(b) (improvement for β near 1), 4(c) (a sufficient condition for optimality), Lemma 2, and 4(d) (a sufficient condition for near optimality).

The mission also states, as intermediate results:

• Lemma 1(a), (c), (d): for every Markov matrix, convergence of the Cesàro means to a Markov $Q^*$ with $QQ^* = Q^*Q = Q^*Q^* = Q^*$; unique solvability of $Qx = x$, $Q^*x = Q^*c$; nonsingularity of $I - Q + Q^*$, $\sum_n \beta^n (Q^n - Q^*) \to H$ and the identities for $H$.
• Theorem 4(a): $V_\beta(f) = x(f)/(1-\beta) + y(f) + o(1)$, with $x(f), y(f)$ the unique solutions of their linear systems; display (2), the same expansion for $(g, f^{(\infty)})$.
• Theorem 3 and its Corollary for fixed $\beta < 1$, and the first assertion of 4(e).

Significance

Theorem 4(e) says that near optimality for β near 1 is exactly lexicographic maximization: first of the average income $x$, then of the bias $y$. It justifies the two-level optimality equations used throughout average-reward dynamic programming and shows that, once the β = 1 improvement routine stops, the remaining problem is a bias maximization over the gain-optimal rules. Theorem 4(a) is the first two terms of the Laurent expansion of discounted values, the starting point of sensitive-discount optimality.

The results are classical and proved in the paper (Lemma 1 with a reference to Kemeny and Snell); no machine-checked proof of them is known on the platform. A complete development produces a multichain theory of Cesàro limit and deviation matrices of arbitrary finite Markov matrices, which Mathlib does not have, and the expansion of discounted returns near β = 1.

Difficulty

Lemma 1 must be proved for every Markov matrix, including reducible and periodic ones, where $Q^n$ does not converge and the stationary distribution is not unique; arguments through the Perron–Frobenius eigenvector of an irreducible chain do not apply. In Theorem 4(e) the hard part is the existence of a single $f^*$ whose bias dominates every gain-optimal rule in every coordinate at once; a rule maximizing each coordinate separately is not enough. The final characterization compares a stationary policy with all policies, including time-dependent ones, through $U(\beta)$.

Formalization scope

States and actions are finite nonempty types; incomes are real of any sign; a policy is a sequence ℕ → (St → Act) with π 0 the paper's $f_1$. $V_\beta$ is a real tsum. $Q^*$ is limUnder of the Cesàro means, and its existence is Lemma 1(a), not an assumption; $H(\beta)$ is a matrix tsum, whose summability for $0 \le \beta < 1$ is part of Lemma 1(d); $H$ uses Mathlib's total inverse, whose nonsingularity is also part of Lemma 1(d). $x(f)$ and $y(f)$ are defined by the closed forms $Q^*(f)r(f)$ and $H(f)r(f)$ from the paper's proof, and Theorem 4(a) asserts that they are the unique solutions of the paper's defining systems. Limits "as β → 1" are along $\beta \to 1^-$. "Nearly optimal" is encoded without $U$: for every $\varepsilon > 0$, for all β in some interval $(\beta_0, 1)$, every policy's return is at most $V_\beta(\pi) + \varepsilon$ in every coordinate; this is equivalent to $U(\beta) - V_\beta(\pi) \to 0$ because a β-optimal policy exists. "Optimal" (§4) and "β-optimal" (§3) are distinct definitions, and Theorem 3's β-dependent improvement set is distinct from the §4 set $G(s,f)$.

A formalization in which optimality or near optimality is tested only against stationary policies, or in which $Q^*$ is assumed to exist or the chain to be irreducible, proves a different and easier theorem and does not meet the targets.

Contributions are welcome at every level: the Cesàro and Abel limit theory of finite Markov matrices (reusable well beyond this paper), the policy improvement theorem for fixed β, and the comparison arguments of Theorem 4. Theorem 3 and the Corollary are also drafted in the companion mission on Theorem 5 in another namespace.

Selected references

• D. Blackwell, Discrete Dynamic Programming, Ann. Math. Statist. 33(2):719–726, 1962. https://doi.org/10.1214/aoms/1177704593
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. G. Kemeny and J. L. Snell, Finite Markov Chains, Van Nostrand, 1960.
• B. L. Miller and A. F. Veinott, Discrete Dynamic Programming with a Small Interest Rate, Ann. Math. Statist. 40(2):366–370, 1969.
• A. F. Veinott, Discrete Dynamic Programming with Sensitive Discount Optimality Criteria, Ann. Math. Statist. 40(5):1635–1660, 1969. https://doi.org/10.1214/aoms/1177697379
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

The classical secretary problem asks how to select one valuable candidate when candidates arrive in random order and a decision must be made when each candidate appears. Many allocation settings have several goods of unequal quality instead of a single position. An employer may have roles of different desirability, or a seller may have placements with different visibility. In the weighted secretary problem, an agent's value is multiplied by the weight of the good assigned to that agent. The algorithm must decide irrevocably as agents arrive, while the benchmark sees every value before assigning goods. Babaioff, Dinitz, Gupta, Immorlica and Talwar study this model with arbitrary fixed agent values and a uniformly random arrival order, and give a constant competitive ratio independent of the number of agents and goods (authors' version, §§2–3).

The paper also studies time discounts and matroid constraints. This mission concerns its weighted-goods result, Theorem 3.4. The result combines an online allocation rule for several comparably valuable agents with the familiar one-choice secretary rule for an unusually valuable agent. These are distinct ways in which the sorted offline assignment can earn value; both are present even when the weights are fixed in advance. The weighted model matters because matching a valuable agent to an unsuitable good can lose value despite accepting the right agent.

Setting

There are $n$ agents $e\in U$, each with a nonnegative value $v(e)$, and $K$ goods indexed in decreasing order of nonnegative weight:

$$w(1)\ge w(2)\ge\cdots\ge w(K)\ge0.$$

An assignment $s$ gives each good to at most one agent, and each agent receives at most one good. A good may remain unassigned, represented by $\bot$ with $v(\bot)=0$. Its value is $\sum_{k=1}^K v(s(k))w(k)$. Agent values are arbitrary, not drawn independently from a distribution. The uncertainty is the arrival order $\pi$, chosen uniformly from all permutations; an agent's value becomes visible on arrival, and an allocation decision cannot be revised.

The offline optimum, $\mathrm{OPT}$, assigns the heaviest good to the highest-valued agent, the next good to the next agent, and so on. If $K>n$, the extra goods remain unassigned. A consistent tie break makes the ordering unique without changing the numerical value. This sorted assignment is defined directly; the mission does not replace it with an unconstrained variable said to be optimal.

The reservation algorithm draws a sample size $\tau\sim\mathrm{Binom}(n,1/2)$, observes the first $\tau$ agents without allocation, and retains the best $\min(K,\tau)$ sampled agents. Positive values are grouped into value classes $[2^{i-1},2^i)$ for integer $i$. A sampled agent in class $i$ reserves one good in that class's contiguous block, with higher classes receiving heavier blocks. A later agent receives the heaviest unassigned good reserved for its class when one is available. The classical secretary rule instead observes the first $\lfloor n/e\rfloor$ agents, then selects the first later arrival better than every predecessor; its winner receives good $1$.

Formalization targets

The mission's goal is the exact guarantee of Theorem 3.4 for Algorithm $A$, which runs the reservation algorithm with probability $8/(3e+8)$ and the classical rule with probability $3e/(3e+8)$:

$$\mathrm{OPT}\le(8+3e)\,\mathbb E[A].$$

Here the expectation covers the uniform arrival permutation, the independent binomial sample size used by the reservation branch, and the mixing coin. The multiplicative inequality expresses competitiveness even when an expected payoff is zero. It uses the explicit constant in the paper's proof rather than an instance-dependent or unspecified constant.

Four source results form the milestones. The classical secretary rule selects the maximum with probability at least $1/e$. Lemma 3.2 compares the starting indices $b_i$ and $o_i$ of class-$i$ blocks in the reservation and optimum assignments. Lemma 3.1 says that if the optimum assigns at least two agents from class $i$, the reservation rule assigns at least $u_i/4$ agents from that class in expectation. Lemma 3.3 converts this to expected value at least $\mathrm{OPT}_i/8$. The target retains the paper's class condition and both numerical fractions (authors' version, pp. 4–5).

Significance

Theorem 3.4 supplies a constant factor guarantee for irrevocable allocation when goods have different weights and agents arrive in random order. The factor does not grow with $n$ or $K$. It separates the effects of uncertain arrivals from the offline matching of high values to high weights, and it supplies a benchmark for later variants with more complicated feasibility constraints. The paper extends the reservation idea to additional combinatorial settings, including partition-matroid variants in Appendix C (authors' version, Appendix C).

The theorem is proved in the source paper, while the Lean statements in this mission are proof obligations. Formalizing them requires checking that the random-order model, sample distribution, tie convention and assignments jointly express the same algorithm. A complete development will also establish reusable finite-average facts for random permutations and binomial samples, and structural facts about sorted assignments and reserved blocks. Those pieces can support other secretary problems in the series; the mission's specific promise remains the weighted algorithm's exact bound.

Difficulty

A count of how many agents a class receives does not by itself control the weighted value of those goods. Goods have unequal weights, and the value of assigning the next good changes with its position in a block. A class whose offline optimum receives several agents can also lose all its sampled members from the allocation phase. Thus a direct comparison of expected class counts with expected class values is insufficient. The paper's separate count, block-position and value statements identify the claims a solver must establish; the final theorem must also account for classes represented only once in the offline assignment (authors' version, p. 5).

Formalization scope

Agents and goods are Fin n and Fin K; their indices start at zero in Lean, so paper time $t$ corresponds to Lean index $t-1$. An arrival permutation maps time to agent. Values and weights are real and explicitly nonnegative, and weights are antitone in the good index. The finite sums defining expectations are normalized by $n!$ for permutations and by $\binom n\tau/2^n$ for sample sizes. No measurability or integration convention is needed. For the goal, $K\ge1$ makes the heaviest good available; $K>n$ is allowed.

Equal values are ordered by smaller original agent index throughout the sorted optimum, the sample's top agents and the classical rule. The classical rule observes exactly $\lfloor n/e\rfloor$ arrivals, and zero-valued agents reserve no value-class goods. Positive values below one use negative integer class indices. The paper says only that class $i$ holds the values “between” $2^{i-1}$ and $2^i$ (p. 4, and again in Appendix C, p. 12); the mission fixes the half-open interval $[2^{i-1},2^i)$, so that the classes partition the positive reals (authors' version, pp. 4, 12). A reservation assignment is built from each post-sample agent's rank within its class, so a good is offered to at most one such agent. The theorem is about this concrete algorithm and the concrete sorted offline assignment; an arbitrary favorable policy or an optimum supplied as a hypothesis would not express the source result.

The development needs a finite assignment interface, a tie-aware rank order, value classes, the two online rules, and normalized finite expectations. The assignment and finite-average definitions are reusable. Contributions that prove the structural validity of the reservation assignment, the classical success guarantee, Lemmas 3.1–3.3, or the final combination all advance the stated target.

Selected references

• Moshe Babaioff, Michael Dinitz, Anupam Gupta, Nicole Immorlica and Kunal Talwar, Secretary Problems: Weights and Discounts, Proceedings of SODA 2009; authors' full version, proceedings DOI.

Motivation

In the secretary problem, $n$ items with nonnegative values arrive one at a time in a uniformly random order, and an online algorithm must decide on each arrival, irrevocably, whether to keep it. The classical version keeps one item; the rule that observes a $1/e$ fraction of the arrivals and then takes the first item better than everything seen picks the best item with probability at least $1/e$ (Ferguson 1989).

Babaioff, Immorlica and Kleinberg (SODA 2007; journal version J. ACM 2018) introduced the matroid secretary problem: the kept set must be independent in a known matroid. It models online auctions in which the feasible sets of winners have matroid structure, for example hiring along the edges of a network without closing a cycle. They gave a $16$-competitive algorithm when the matroid is graphic, i.e. the items are the edges of a graph and a set is feasible when it contains no cycle.

Timeline for graphic matroids:

• 2007, Babaioff–Immorlica–Kleinberg: $16$-competitive.
• 2009, Babaioff–Dinitz–Gupta–Immorlica–Talwar (SODA 2009, Theorem 1.5): $3e\approx 8.15$-competitive, through a random reduction to partition matroids. This mission formalizes that result.
• 2009, Korula–Pál (ICALP 2009): $2e$-competitive, by a different reduction.

Setting

Let $G=(V,E)$ be a finite simple graph. Each edge $e$ has a value $v(e)\ge 0$. A set $S\subseteq E$ is independent in the graphic matroid of $G$ if the graph $(V,S)$ has no cycle. The offline optimum is

$$\mathrm{OPT}(G,v)=\max\Big\{\sum_{e\in S}v(e): S\subseteq E\ \text{acyclic}\Big\}.$$

The edges arrive in a uniformly random order. An algorithm sees each edge and its value on arrival and decides at once whether to select it. The selected set must be acyclic. The algorithm is $\alpha$-competitive if $\mathrm{OPT}(G,v)\le\alpha\cdot\mathbb E[\text{value of the selected set}]$ for every $G$ and every $v\ge 0$.

A partition matroid on a subset $U'\subseteq E$ is given by a family $P$ of nonempty, pairwise disjoint parts with union $U'$: a set is independent when it lies in $U'$ and meets each part at most once. Its max-weight base has value $\mathrm{val}(P,v)=\sum_{p\in P}\max_{e\in p}v(e)$.

Definition 5.1. A random partition $\mu$ (a probability distribution on such families, chosen from $G$ alone) is an $\alpha$-partition scheme if every partition in its support has only acyclic independent sets, and for every $v\ge 0$,

$$\mathrm{OPT}(G,v)\le \alpha\cdot\mathbb E_{P\sim\mu}[\mathrm{val}(P,v)].$$

The random partition of Lemma 5.3. Pick an edge $\{u,w\}$ uniformly at random. With probability $\tfrac12$ colour $u$ red and $w$ blue, otherwise the reverse. Colour every other vertex red or blue independently with probability $\tfrac12$. Each red vertex $x$ gets a part: the red-blue edges at $x$. Then repeat on the edges with both endpoints blue, with fresh randomness.

The algorithm. Draw the partition, let the edges arrive, and on each part run the classical secretary rule on that part's arrivals. Output all selected edges.

Formalization targets

Goal: Theorem 1.5

For every finite simple graph $G$ and every $v\ge 0$:

1. every possible output of the algorithm is an acyclic set of edges of $G$;

$$\mathrm{OPT}(G,v)\le 3e\cdot\mathbb E[\mathrm{ALG}].$$

Part 1 is needed for the statement to have content: an algorithm that selects every edge would otherwise satisfy part 2.

Milestones

• Section 2, p. 4. On $m\ge1$ arrivals, the classical rule selects the maximum with probability at least $1/e$.
• Theorem 5.4, first clause. For a fixed partition $P$, the per-part rule outputs a set independent in the partition matroid, and $\mathrm{val}(P,v)\le e\cdot\mathbb E_\pi[\mathrm{ALG}]$.
• Lemma 5.3, independence. Every partition the random construction can produce is a partition matroid on a subset of $E$, and each of its independent sets is a forest.
• Lemma 5.3. The construction is a $3$-partition scheme.
• Section 5, p. 10. Any $\alpha$-partition scheme for a graphic matroid, combined with the per-part rule, gives a feasible, $e\alpha$-competitive algorithm.

Significance

The theorem shows that the graphic matroid secretary problem admits a constant-competitive algorithm with a small explicit constant. It does so through a reduction: a random partition matroid that is feasible for the original matroid and loses only a constant factor in expectation. The reduction separates the combinatorics (Lemma 5.3) from the online part (Theorem 5.4). The same framework gives algorithms for uniform and transversal matroids and for the weighted and discounted variants on any matroid with an $\alpha$-partition property.

The result is proved in the paper; it has not been formalized. The mission contributes a machine-checked version of the reduction, a formal treatment of a recursively defined random partition, and the classical secretary bound in a reusable finite form. The constant $3e$ is not the best known for graphic matroids (Korula–Pál improve it to $2e$), so the formal goal is this algorithm's guarantee, not the best possible ratio.

Difficulty

The online half is routine once the classical bound is available: the relative order of the edges in each part is uniform, and the parts are disjoint. The difficulty is Lemma 5.3. The natural idea of using a fixed optimal forest to build the partition is ruled out because the partition must be chosen before the values are seen. The expectation bound must therefore hold for every valuation at once, for a law that depends on the graph only. The construction is recursive and random: its expected value is not a closed-form sum, and any bound has to be carried through the random sequence of blue-blue subgraphs. Feasibility needs an invariant across rounds: the parts created later live inside the blue-blue edges of every earlier round.

Formalization scope

• Graph. A SimpleGraph on a Fintype vertex type with decidable adjacency. The edges are G.edgeFinset, and acyclicity of $S$ is (SimpleGraph.fromEdgeSet S).IsAcyclic. Multigraphs are not covered.
• Values. Values are a real function v : Sym2 V → ℝ with ∀ e, 0 ≤ v e; only the values on edges matter.
• OPT is a Finset.sup' over acyclic subsets of the edge set. A partition is a finite family of nonempty, pairwise disjoint parts inside the edge set. Its max-weight base value is the sum of the part maxima.
• Random partition. A PMF defined by well-founded recursion on the number of edges. Empty parts are dropped, and edges with two red endpoints are discarded.
• Random order. The edges are numbered by a fixed enumeration. An arrival order is a permutation of the numbers, and expectation over the order is the average over all $|E|!$ permutations.
• Classical rule. It samples $\lfloor m/e\rfloor$ arrivals of a part with $m$ edges. Ties are broken by preferring the smaller edge number among equal values.
• Constants. Competitiveness is multiplicative ($\mathrm{OPT}\le 3e\cdot\mathbb E[\mathrm{ALG}]$), so a zero expectation is not a loophole.
• Ruling out trivial formalizations. In Definition 5.1 the random partition is fixed before the valuation, and the independence requirement holds for every partition in its support. A partition allowed to depend on $v$ would make every matroid $1$-partitionable.

A complete development needs the classical secretary bound in finite form, the uniformity of induced sub-orders of a uniform permutation, expectations of PMF.bind along a well-founded recursion, and facts about forests in SimpleGraph. The first two, and a general graphic-matroid layer, are reusable beyond this mission. Proofs of any milestone, alternative proofs of Lemma 5.3, and extensions to the uniform and transversal cases of Theorem 5.2 are welcome.

Selected references

• M. Babaioff, M. Dinitz, A. Gupta, N. Immorlica, K. Talwar, Secretary Problems: Weights and Discounts, Proc. 20th ACM-SIAM Symposium on Discrete Algorithms (SODA), 2009. https://doi.org/10.1137/1.9781611973068.135
• M. Babaioff, N. Immorlica, R. Kleinberg, Matroids, secretary problems, and online mechanisms, SODA 2007, pp. 434–443. https://dl.acm.org/doi/10.5555/1283383.1283429
• M. Babaioff, N. Immorlica, D. Kempe, R. Kleinberg, Matroid Secretary Problems, Journal of the ACM 65(6), 2018. https://doi.org/10.1145/3212512
• N. Korula, M. Pál, Algorithms for Secretary Problems on Graphs and Hypergraphs, ICALP 2009, LNCS 5556. https://doi.org/10.1007/978-3-642-02930-1_42
• T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 1989. https://doi.org/10.1214/ss/1177012493