Probability

Motivation

In hiring, admissions and procurement, candidates are often judged by scores that are known to be biased: two candidates from different groups, schools or evaluation pipelines cannot be compared by their observed scores, while two candidates from the same pipeline can. Salem and Gupta (SSRN 3444283, published in Management Science, 2023) model this situation as a poset secretary problem. The decision maker sees only a partial order between candidates, namely the comparisons that are trustworthy, and must still make irrevocable online selections.

The classical secretary problem and its $k$-selection variant (Kleinberg, 2005) assume a total order. With only partial comparisons, the natural question is how much the missing comparisons cost. Salem and Gupta answer it in terms of the width of the poset. This mission formalizes their lower bound: no algorithm can do better than a factor of the width.

Setting

A finite set $\mathcal C$ of $N$ candidates carries a partial order $\preceq$. Each candidate $a$ has a true score $w(a)$. The scores are nonnegative and pairwise distinct, and they are consistent with the order: $a\prec b$ implies $w(a)<w(b)$. The pair $\mathcal I=(\mathcal P,w)$ is an instance. Candidates arrive in uniformly random order. An algorithm knows $N$ and a capacity $k$, observes the comparisons of $\mathcal P$ among the candidates that have arrived, and selects at most $k$ candidates, irrevocably. It never observes the scores.

The offline optimum is

$$\mathrm{OPT}(w,k)=\max\Big\{\textstyle\sum_{a\in S}w(a)\;:\;S\subseteq\mathcal C,\ |S|\le k\Big\}.$$

An algorithm is $\alpha$-competitive if $\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\mathrm{OPT}(\mathcal I)/\alpha$ on every instance (Definition 3.4).

The width $\omega$ of $\mathcal P$ is the largest number of pairwise incomparable candidates (an antichain).

Because an algorithm sees only the poset and the arrival order, on a fixed poset its randomness (arrival order and internal coins) induces a probability distribution $\mu$ on the selected set, supported on sets of at most $k$ elements, and $\mu$ does not depend on the scores. Such a $\mu$ is called a selection rule with capacity $k$. Its expected score is $\mathbb E_\mu[w(\mathrm{Alg})]=\sum_S\mu(S)\sum_{a\in S}w(a)$. The selection probability of $a$ is $p(a)=\sum_{S\ni a}\mu(S)$.

The instance of the lower bound is $\mathrm{Chains}(\omega,k)$: $\omega$ disjoint chains of $k$ elements each, with elements in different chains incomparable (Figure 8 of the paper, with $n=\omega k$).

Formalization targets

Goal: Proposition 5.1 (p. 14, proof in Appendix F, p. 42)

For every $k\ge1$ and $\omega\ge1$ there is a poset $\mathcal P$ of width $\omega$ such that for every selection rule $\mu$ with capacity $k$ and every $\varepsilon>0$ there is a consistent scoring $w$ with $\mathrm{OPT}(w,k)>0$ and

$$\mathbb E_\mu[w(\mathrm{Alg})]\le\frac{(1+\varepsilon)\,\mathrm{OPT}(w,k)}{\omega}.$$

Equivalently, for every algorithm, $\sup_{\mathcal I}\mathrm{OPT}(\mathcal I)/\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\omega$, the supremum taken over the scorings of $\mathcal P$.

Milestones (Appendix F, p. 42)

1. The width of $\mathrm{Chains}(\omega,k)$ is $\omega$ for $k\ge1$.
2. For every selection rule with capacity $k$ on $\mathrm{Chains}(\omega,k)$, some chain $i$ has $\sum_j p^i_j\le k/\omega$.
3. If $w$ is a consistent perturbation of the scoring that gives $M/k$ to each element of one chain $i_0$ and $0$ elsewhere, with perturbations below $M/2k$ in absolute value, nonnegative off $i_0$, and summing to $0$ on $i_0$, then $\mathrm{OPT}(w,k)=M$.
4. Given such a chain $i_0$, $M>0$ and $\varepsilon>0$, there is a consistent scoring with $\mathrm{OPT}=M$ and $\mathbb E_\mu[w(\mathrm{Alg})]\le(1+\varepsilon)\mathrm{OPT}/\omega$.

Significance

The result shows that the width of the poset is a genuine barrier: whatever the algorithm, an adversary choosing scores after seeing how the algorithm spreads its selections can force a ratio arbitrarily close to $\omega$. The paper's ProxyLabel algorithm has competitive ratio at most $e(\omega+1)/(1-1/k)^{k-1}\le e^2(\omega+1)$ when the width is known (Corollary 5.1, p. 15). Together the two results show that the best achievable competitive ratio in the poset secretary problem is of order $\omega$, which the paper calls order-optimal. The lower bound also covers the group-bias model of the paper: $\omega$ groups whose members are compared only within their group form exactly the instance used here.

On the formal side, the result is proved in the paper but has no machine-checked proof. The mission produces a formal model of score-independent randomized selection on a finite poset, a formal offline optimum with $k$ selections, and the width of a disjoint union of chains. These can be reused for other lower bounds in online selection.

Difficulty

The argument is short, and the work lies in getting the quantifiers and the encoding right. The printed statement places "there is an instance" before "for any algorithm". Read literally this is false for $\omega\ge2$: on a fixed instance, the algorithm that always selects the $k$ highest-scoring elements achieves ratio $1$. The proof establishes the other order: the poset is fixed, then the algorithm, then the scoring. A formalization must keep the scoring chosen after the algorithm while preventing the algorithm from depending on the scores.

The printed chain of inequalities also needs care. Its middle step drops the term $\sum_j p^\omega_j\varepsilon^\omega_j$, which the stated constraints on the perturbation do not make nonpositive. The bound therefore holds for perturbations chosen small enough, not for every perturbation satisfying the printed constraints. The existence of distinct, order-consistent scores meeting all the constraints at once has to be shown, and so does the identification of the optimum with the heavy chain.

Formalization scope

Elements form a finite type with a partial order. A consistent scoring is a function to $\mathbb R$ that is nonnegative, injective and strictly monotone ($a<b\Rightarrow w(a)<w(b)$). These are the standing assumptions of the model (§3.1, p. 7), not additions. $\mathrm{OPT}$ is a finite maximum over subsets of at most $k$ elements. Width is the published definition AppliedComb.Posets.width, the size of a largest antichain, not a minimum number of chains, so the width milestone is a real claim. Algorithms are represented by selection rules: nonnegative weights on subsets summing to $1$ and vanishing on subsets of more than $k$ elements. This class contains the selected-set law of every online algorithm, so a lower bound for it is a lower bound for online algorithms. Expectations and probabilities are finite sums. Competitiveness is stated as $\mathbb E\le(1+\varepsilon)\mathrm{OPT}/\omega$ together with $\mathrm{OPT}>0$, with no division by an expectation that may vanish. The hypotheses $k\ge1$ and $\omega\ge1$ are standing: with $\omega=0$ the poset is empty, and with $k=0$ every ratio is $0/0$. The instance is the sigma type $\Sigma\,(i:\mathrm{Fin}\,\omega),\mathrm{Fin}\,k$ with Mathlib's disjoint order.

Trivializing formalizations are ruled out explicitly. A selection rule must have total mass $1$, so the zero rule does not make the expected score vanish. It must respect the capacity, so the rule selecting everything is excluded. The scoring is quantified after the selection rule, never before it and never as an input to it. $\mathrm{OPT}>0$ is part of the conclusion.

The development needs finite sums over subsets, the order on sigma types, and antichains. Contributions are welcome on any milestone. The width of a disjoint union of chains and the pigeonhole bound on selection probabilities are reusable beyond this mission.

Selected references

• J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, Management Science, 2023. Preprint: SSRN 3444283 (version of 2022-04-17), https://ssrn.com/abstract=3444283. Published version: https://doi.org/10.1287/mnsc.2023.4926
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of SODA, 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51(1), 1950. https://doi.org/10.2307/1969503

Why investment races matter

Two firms developing competing innovations face a decision that a single firm does not: a rival's discovery can end the value of continuing the project. If the first discovery wins the payoff, each firm chooses how much to spend per period while knowing that greater spending may change both its payoff on success and its speed of discovery. The investment decision therefore depends on what the rival chooses. Danmo Lin's model separates these two channels and asks when competition itself raises a firm's chosen R&D intensity Lin (2022).

This mission concerns the paper's race of two financially unconstrained firms. The result is a comparative statics claim about a firm's best response to its rival, together with existence of a symmetric pure-strategy equilibrium. The paper proves the result in Appendix A.6. The problem here is to give machine-checked statements and ultimately a proof for the same stochastic race, including its strategy ranges and first-arrival payoffs.

The two-firm race

Firm $i\in\{1,2\}$ chooses a fixed investment intensity $R_i$, the amount it pays per unit time while the race continues. Its technology has parameters $(A_i,\beta_i,\eta_i,\gamma_i)$. If it discovers first, its mean project payoff is $u_i(R_i)=A_iR_i^{\beta_i}$. Its discovery time $\tau_i$ is exponentially distributed with rate $\lambda_i(R_i)=\eta_iR_i^{\gamma_i}$. The discovery times are independent, represented by the product law $\mathcal E(\lambda_1,\lambda_2)$, and the earlier discovery wins. Both firms stop paying at $\min\{\tau_1,\tau_2\}$. The loser receives no discovery payoff. Future cash flows are discounted at rate $r>0$ Lin (2022), §3.1.

The technology conditions are $A_i,\eta_i>0$, $0\le\beta_i,\gamma_i<1$, and $\beta_i+\gamma_i<1$. A project is scalable when its discovery payoff increases with investment, corresponding here to $\beta_i>0$. It is accelerable when investment increases its discovery rate, corresponding to $\gamma_i>0$. The model permits the two firms' parameters to differ. The lower intensity is $1$; the upper intensity is $\bar R_i=(A_i\eta_i)^{1/(1-\beta_i-\gamma_i)}$. The standing condition $A_i\eta_i>1$ makes $[1,\bar R_i]$ a nondegenerate range in which investment takes place Lin (2022), (2), (7).

Write $P_i(R_1,R_2)$ for Firm $i$'s expected discounted payoff from the first-arrival race. Its best-response set $BR_i(R_{-i})$ contains every maximizer of $P_i$ over its own fixed interval $[1,\bar R_i]$, holding the rival's intensity fixed. A pure Nash equilibrium is a pair $(R_1,R_2)$ in which each intensity belongs to that firm's best-response set. This set-valued definition keeps the claim meaningful when there is more than one maximizer.

Formalization targets

The first milestone identifies each expected payoff with the closed form in Lemma 2:

$$P_i(R_1,R_2)=V_i(R_1,R_2) =\frac{u_i(R_i)\lambda_i(R_i)-R_i}{r+\lambda_1(R_1)+\lambda_2(R_2)}.$$

The second milestone is the Appendix A.6 cross-partial identity. For Firm 1, the expression $V_1\,\partial^2_{R_1R_2}V_1-(\partial_{R_1}V_1)(\partial_{R_2}V_1)$ equals $\lambda'_2(u_1\lambda_1-R_1)^2\lambda'_1/(r+\lambda_1+\lambda_2)^4$. It is strictly positive when both discovery rates rise with intensity and Firm 1's project surplus is nonzero Lin (2022), (A.27)–(A.28).

The goal is Proposition 3. When both projects are accelerable, higher rival investment orders the best-response sets upward, with strict movement for an old response above $1$. When neither project is accelerable, the best-response sets are constant in the rival's intensity. For identical firms, the theorem asserts a symmetric pure Nash equilibrium:

$$\exists R\in[1,\bar R]\quad R\in BR_1(R)\cap BR_2(R).$$

Best-response sets are required to be nonempty for every positive rival intensity. The ordering statements therefore make substantive claims about actual choices Lin (2022), Proposition 3.

What the result establishes

The result distinguishes a change in the timing of innovation from a change in its eventual payoff. In an accelerable project, a rival who spends more discovers faster, and the firm's optimal investment response moves upward. If investment cannot affect discovery speed, a rival's intensity does not alter the firm's best-response set in this model. The equilibrium clause says the symmetric game has at least one profile at which neither firm gains by changing its own intensity. These are statements about competition's effect on project spending, rather than only about the numerical value of a firm Lin (2022), §3.1.

The mathematical result is proved in the paper; the mission seeks a Lean formalization of that known result. The expectation-to-value identity requires a reusable treatment of independent exponential discovery times and discounted spending stopped at the first arrival. The best-response statement then supplies a precise set-valued comparative statics target. A verified development of these ingredients could be reused for other innovation races and first-arrival games. This mission does not claim that such a machine-checked proof already exists.

Mathematical difficulty

The payoff is an expectation over two random times, with the prize awarded only to the earlier discovery and spending stopped at their minimum. The closed form must agree with that stochastic expression for each positive pair of intensities. The comparison of best responses involves all maximizers, including possible ties and boundary choices. A derivative of one selected optimizer is not a well-defined substitute when the optimizer is set-valued; moreover, strict response cannot be demanded at the lower endpoint. Equilibrium existence must hold for the same best-response correspondence that defines the competitive race. These points make a direct translation of the paper's derivative notation insufficient Lin (2022), Appendix A.5–A.6.

Formalization scope

Lean uses real intensities, real technology parameters, Real.rpow for the power functions, and ProbabilityTheory.expMeasure for each discovery time. Their product measure encodes independence. Firm 1's discovery time is the first coordinate throughout, including Firm 2's payoff. The two firms have separate technology records. A best response maximizes the expectation from (8) over the own interval $[1,\bar R_i]$; that interval never depends on the rival's action. The named closed form $V_1$ is separate from the expectation and appears in the Appendix A.6 milestone. The random payoff on discovery is represented by its mean $u_i(R_i)$, as the paper's calculation uses only that mean. The other cash-flow component of the underlying firm value is independent of the R&D choice and is omitted from the race payoff.

The hypotheses $A_i\eta_i>1$, $r>0$, and positive intensities are explicit. The comparison allows any positive rival intensity, while each firm's own maximization uses (7). The paper's derivative claims about $R_i^*$ are posed as orderings of complete best-response sets; strictness is asserted for an old response above $1$. Both firms must be accelerable for the increasing-response clause, and the symmetric equilibrium clause applies to identical technologies. The strict inequality in (A.28) includes the necessary nonzero-surplus condition, since its square vanishes at the upper endpoint. These choices and the printed endpoint issue are recorded in the mission's moderation notes.

The target excludes empty best-response sets, rival-dependent feasible ranges, payoffs defined by the closed form (9), an equilibrium asserted without mutual best-response membership, and comparisons that discard the strict interior part. A complete development will need integration and exponential-distribution facts, continuity and maximizer existence on compact intervals, ordered best-response sets, and a fixed-point argument for the symmetric correspondence. The first-arrival probability and integration results can be reused beyond this paper; contributions to those interfaces and to the two stated milestones are welcome.

Selected references

• Danmo Lin, Accelerability vs. Scalability: R&D Investment Under Financial Constraints and Competition, Management Science, Articles in Advance, 2022. DOI: 10.1287/mnsc.2022.4503.

Why impact-ranked portfolios can earn excess returns

Impact investing selects securities by a non-financial score, an ESG rating, a carbon intensity, a measure of social benefit, and asks whether such a selection earns an excess return. A. W. Lo and R. Zhang (SSRN 3944367; published in Management Science, DOI 10.1287/mnsc.2022.01168) model the score as an impact factor $X$ and study the returns of securities ranked by $X$ with the tools of induced order statistics (concomitants), introduced by Bhattacharya (1974) and David (1973).

Section 4.3 of the paper gives an equilibrium reading of the apparent excess return. In a $K$-factor asset-pricing model with no mispricing, an investor who accounts only for the first factor sees the contribution $\lambda_i$ of the omitted factors $2,\dots,K$ to security $i$'s return as alpha. If the impact factor is correlated with these omitted factors, ranking by impact selects omitted-factor risk, and the selected portfolio appears to earn an excess return. Empirical studies of sin stocks (Blitz and Fabozzi, 2017) and ESG scores (Madhavan, Sobczyk and Ang, 2021) report exactly this effect. Proposition 5 quantifies it in closed form.

Setting

There are $N$ securities. For security $i$, $X_i$ is its impact factor and $\lambda_i$ the total net contribution of the omitted factors to its return. Write $X = (X_1,\dots,X_N)$ and $\lambda = (\lambda_1,\dots,\lambda_N)$, random vectors on a probability space $(\Omega,\mathcal F, P)$.

Order statistics. Sorting the entries of $X$ increasingly gives $X_{1:N} \le \dots \le X_{N:N}$, the order statistics of $X$. If $\pi$ is the sorting permutation, $X_{i:N} = X_{\pi(i)}$, and the induced order statistic $\lambda_{[i:N]} = \lambda_{\pi(i)}$ is the omitted-factor return of the security with the $i$-th smallest impact factor. The order is induced by $X$, never by $\lambda$ (display (6), p. 11).

Assumption (A2) (p. 19). The vector $(X,\lambda)$ is Gaussian with exchangeable first and second moments: $\mathbb E[X_i] = \mu_x$, $\mathbb E[\lambda_i] = \mu_\lambda$, $\mathrm{Var}(X_i) = \sigma_x^2$, $\mathrm{Var}(\lambda_i) = \sigma_\lambda^2$, $\mathrm{Corr}(X_i,\lambda_i) = \rho_{x,\lambda}$, and for $i \ne j$, $\mathrm{Corr}(X_i, X_j) = \rho_x$, $\mathrm{Corr}(\lambda_i,\lambda_j) = \rho_\lambda$, $\mathrm{Corr}(X_i,\lambda_j) = \tilde\rho_{x,\lambda}$. The paper normalises $\mu_x = 0$ and $\sigma_x = 1$ and keeps a free premium $\mu_\lambda$. The adjusted correlation is

$$\rho_{adj} = \frac{\rho_{x,\lambda} - \tilde\rho_{x,\lambda}}{1-\rho_x}. \qquad (24)$$

Formalization targets

Goal: Proposition 5 (pp. 19–20)

Under (A2), for every rank $i$ and every pair of ranks $i \ne j$,

$$\mathbb E[\lambda_{[i:N]}] - \mu_\lambda = \rho_{adj}\sigma_\lambda\,\mathbb E[X_{i:N}], \qquad (25)$$ $$\mathrm{Var}(\lambda_{[i:N]}) = \sigma_\lambda^2\big(1-\rho_{adj}^2 + \rho_{adj}^2\,\mathrm{Var}(X_{i:N})\big), \qquad (26)$$ $$\mathrm{Cov}(\lambda_{[i:N]},\lambda_{[j:N]}) = \sigma_\lambda^2\rho_{adj}^2\,\mathrm{Cov}(X_{i:N},X_{j:N}) + \sigma_\lambda^2\big(\rho_\lambda - \rho_x\rho_{adj}^2\big). \qquad (27)$$

The goal states (27) with the factor $\sigma_\lambda^2$ on the last term. The paper prints $(\rho_\lambda - \rho_x\rho_{adj}^2)$ without it. That is a slip: replacing $\lambda$ by $c\lambda$ with $c>0$ multiplies the left side by $c^2$ and leaves every correlation unchanged, so the printed formula fails whenever $\sigma_\lambda \ne 1$. With $a = \rho_{adj}\sigma_\lambda$, the correct value is $\rho_\lambda\sigma_\lambda^2 + a^2(\mathrm{Cov}(X_{i:N},X_{j:N}) - \rho_x)$, which is the goal's right side.

Milestones

1. (A.42)–(A.43), p. 68: with $\mathbf P = a\mathbf I + b\mathbf L$, $\mathbf L = \mathbf 1\mathbf 1^{\mathsf T}/N$, $a = \rho_{adj}\sigma_\lambda$ and $b = \big(\frac{\rho_{x,\lambda} + (N-1)\tilde\rho_{x,\lambda}}{1+(N-1)\rho_x} - \rho_{adj}\big)\sigma_\lambda$, the residual $\lambda - \mathbf P X$ is independent of $X$.
2. (A.44) = (25), p. 68: the mean formula.
3. (26), p. 20: the variance formula.

Significance

The result. Proposition 5 shows that the apparent alpha of the security ranked $i$-th by impact is $\mu_\lambda + \rho_{adj}\sigma_\lambda\mathbb E[X_{i:N}]$. A selection rule that looks unrelated to return characteristics still produces nonzero excess returns when it is correlated with omitted priced factors, and the size of the effect is governed by the single number $\rho_{adj}$. The authors use this to argue that impact estimates are unreliable until all known factors are accounted for, and that a persistent impact premium may signal a new factor (an "ESG factor" or a "carbon factor"). The variance and covariance formulas give the risk of any portfolio of impact-ranked securities, through the moments of Gaussian order statistics.

Formalizing it. The paper proves (25) in full and states that (26)–(27) "can be proven similarly"; the printed (27) is off by the factor $\sigma_\lambda^2$. A machine-checked proof settles the corrected constants. No part of this result, and no theory of induced order statistics, is formalized in Lean or elsewhere to our knowledge. The development needs a usable library on concomitants of Gaussian order statistics, which would serve the rest of the paper (Propositions 2, 4 and 6) and the data-snooping analysis of Lo and MacKinlay (1990), which uses the same tools.

Difficulty

The mean formula looks like linearity of expectation, but $\lambda_{[i:N]} = \lambda_{\pi(i)}$ is evaluated at a random index $\pi(i)$ that depends on $X$, so $\mathbb E[\lambda_{\pi(i)}]$ is not $\mathbb E[\lambda_k]$ for any fixed $k$. The decomposition of milestone 1 is what handles this. It requires the full joint Gaussian law of $(X,\lambda)$, because uncorrelated is not independent otherwise. It also needs a correction term $b\bar X$ through the cross-sectional average, because the cross-correlations $\rho_x$ and $\tilde\rho_{x,\lambda}$ make $\mathbb E[\lambda \mid X]$ depend on all of $X$. In Lean, the sorting permutation must be shown measurable in $X$, and the moments of the order statistics must be shown finite.

Formalization scope

• $X$ and $\lambda$ are families Fin N → Ω → ℝ on a probability space. (A2) is the predicate IsA2: joint Gaussianity of the $2N$-vector (Mathlib's HasGaussianLaw on (Fin N → ℝ) × (Fin N → ℝ)), plus the moments (22)–(23) stated as covariances with $\sigma_x = 1$.
• Joint Gaussianity. (A2) as printed asks only that each pair $(X_i,\lambda_i)$ be bivariate normal. The proof (A.40) treats $(X,\lambda)$ as one Gaussian vector that "completely characterizes the joint distribution". The joint reading is the one formalized; under pairwise normality alone the results fail in general.
• Normalisations are hypotheses. $\mu_x = 0$ and $\sigma_x = 1$ (the paper's "without loss of generality") are fields of IsA2. $\mu_\lambda$ is free.
• Added parameter hypotheses. $\sigma_\lambda > 0$ (implicit in "correlation") and $\rho_x < 1$ (implicit in the division in (24)). No positive-semidefiniteness condition is added: it follows from the existence of the random vector.
• Ranks are 0-based (Fin N): Lean's rank $i$ is the paper's $i+1$. Sorting uses Tuple.sort, which breaks ties by index; ties have probability zero and the statements hold for any tie-breaking rule. Moments are Mathlib's integral, variance and covariance. The milestones use $N$ where the page writes $n$ in $(n-1)$.
• Trivializing readings are ruled out. The hypotheses are satisfiable for every $N$: a sanity file builds a witness from a standard Gaussian vector. All variables are Gaussian or bounded by Gaussians, so no expectation is Lean's junk value $0$ for a non-integrable function.
• Out of scope: the multi-factor return model beyond the definition of $\lambda$; Proposition 2 and the impact-portfolio results (a separate mission); Treynor–Black weights (Proposition 7); combined portfolios (Proposition 8); asymptotic statements (Propositions 3, A.1, A.2).
• Contributions welcome: measurability of Tuple.sort as a function of the data; integrability and moments of Gaussian order statistics; moments of a vector independent of $X$ read at an $X$-dependent random index. Each of these is reusable well beyond this mission.

Selected references

• A. W. Lo and R. Zhang, Quantifying the Impact of Impact Investing, SSRN 3944367, draft of 29 June 2023; Management Science. https://ssrn.com/abstract=3944367, https://doi.org/10.1287/mnsc.2022.01168
• P. K. Bhattacharya, Convergence of Sample Paths of Normalized Sums of Induced Order Statistics, Annals of Statistics 2(5), 1974.
• H. A. David, Concomitants of Order Statistics, Bulletin of the International Statistical Institute 45, 1973. (No DOI.)
• A. W. Lo and A. C. MacKinlay, Data-Snooping Biases in Tests of Financial Asset Pricing Models, Review of Financial Studies 3(3), 1990. https://doi.org/10.1093/rfs/3.3.431
• D. Blitz and F. J. Fabozzi, Sin Stocks Revisited: Resolving the Sin Stock Anomaly, Journal of Portfolio Management 44(1), 2017.
• A. Madhavan, A. Sobczyk and A. Ang, Toward ESG Alpha: Analyzing ESG Exposures through a Factor Lens, Financial Analysts Journal 77(1), 2021.

Motivation

Two-sided platforms for dating, freelancing and housing do more than list participants: they decide whom each participant is shown. When search is costly and agents leave the market over time, the platform's choice of assortments (which types of agents meet which, and how often) determines who matches, and agents respond strategically by deciding which matches to accept. A platform that ignores those responses can design meetings that agents then decline.

Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search in a stationary flow economy and ask how much welfare a platform can secure when it controls only meetings, while agents retain the decision to accept. Computing the optimal assortments is NP-hard to approximate within 24/23 (their Theorem 4.2), so the relevant question is whether a constant fraction of the best conceivable welfare is reachable at all. Their Theorem 4.1 answers it with the factor 4, measured against the platform's first best, a benchmark in which the platform also dictates acceptance.

The mission formalizes the existence part of Theorem 4.1 and the chain of results in §4 of the paper that leads to it.

Setting

There are finitely many types on two sides, a set $\mathcal M$ and a set $\mathcal W$; write $\Theta=\mathcal M\cup\mathcal W$ and let $\theta'$ denote a generic type on the side opposite to $\theta$. Agents of type $\theta$ enter at rate $\alpha_\theta>0$ and each agent leaves unmatched at rate $\delta>0$. When an agent of type $m$ meets one of type $w$, both observe one symmetric utility $u$ drawn from a law $F_{mw}$ on $\mathbb R$ with no atoms and finite mean; they match, and leave with utility $u$ each, if both accept.

The platform picks an assortment $\lambda_\theta(\theta')\ge0$ for each type: type $\theta$ meets type $\theta'$ at rate $\lambda_\theta(\theta')$. Agents use thresholds $\tau_\theta$ and accept exactly when $u\ge\tau_\theta$, so a pair matches when $u\ge\max(\tau_m,\tau_w)$. With population masses $\eta_\theta$ and matching rates $\xi_\theta$, the assortments induce a stationary equilibrium when, for every type,

$$\alpha_\theta=(\delta+\xi_\theta)\eta_\theta,\qquad \eta_m\lambda_m(w)=\eta_w\lambda_w(m),\qquad \sum_{\theta'}\lambda_\theta(\theta')\le1,$$ $$\xi_\theta=\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty dF_{\theta\theta'},\qquad \tau_\theta=\frac{\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty u\,dF_{\theta\theta'}}{\delta+\xi_\theta}.$$

These are constraints (6a)–(6f) of the paper; the last one, (6e), says each threshold equals the type's expected utility, which is the agents' best response. The welfare is the flow of realized utility,

$$\mathrm{SW}=\sum_{m}\sum_{w}\big(\eta_m\lambda_m(w)+\eta_w\lambda_w(m)\big)\int_{\max(\tau_m,\tau_w)}^\infty u\,dF_{mw}.$$

The first-best relaxation (§4.1) drops (6e) and replaces $\max(\tau_m,\tau_w)$ by a free pairwise threshold $\tau_{mw}$: the platform chooses both the meetings and which matches happen. Its welfare $\mathrm{FB}$ is the same expression with $\tau_{mw}$.

Formalization targets

Goal: Theorem 4.1

For every market satisfying the standing assumptions there are assortments, thresholds, rates and masses satisfying (6a)–(6f) such that, for every first-best feasible candidate $Q$,

$$\mathrm{FB}(Q)\le 4\,\mathrm{SW}.$$

Milestones

1. Proposition 4.4. The first best equals the linear program $\max\,2\sum_{m,w}\rho_{mw}\beta_{mw}$ subject to $\beta\ge0$, $\sum_w\beta_{mw}\le\alpha_m$, $\sum_m\beta_{mw}\le\alpha_w$, where $\rho_{mw}=\max_{\tau\ge0}\int_\tau^\infty u\,dF_{mw}/(\delta+\int_\tau^\infty dF_{mw})$.
2. Lemma 4.5. The maximizer of $A(\tau)=\int_\tau^\infty u\,dF/(\delta+\int_\tau^\infty dF)$ over $\tau\ge0$ is a fixed point of $A$, and $A$ increases before it and decreases after it.
3. Lemma 4.6. The LP has an optimal solution whose support is a forest on $\Theta$.
4. Lemma 4.7. An edge-weighted forest keeps half its weight on a union of vertex-disjoint stars.
5. Lemma 4.9. In a star-shaped market (one side has a single type) the LP is a fractional knapsack with a greedy optimum.
6. §4.2.2 remark, Lemmas 4.10–4.12. The idealized thresholds $\hat\tau_{w_i}$ exist, coincide with or lie below $\rho_{mw_i}$, and bound the equilibrium thresholds from above and the pair thresholds $\max(\tau_m,\tau_{w_i})$ from below.
7. Proposition 4.8. In a star-shaped market some induced stationary equilibrium satisfies $\mathrm{FB}(Q)\le2\,\mathrm{SW}$ for every first-best feasible $Q$.

Significance

Theorem 4.1 is a price-of-anarchy statement for platform design: restricting the platform to meetings, and letting agents choose acceptance selfishly, costs at most a factor 4 against a platform that dictates everything. Since every equilibrium candidate is also a first-best candidate with the same welfare, it gives a 4-approximation to the optimal directed search as well. The construction behind it has a structure that is itself informative: the equilibrium consists of disjoint submarkets in each of which one side has a single type.

The results are proved in the paper; none of them has a machine-checked proof in Lean or another proof assistant on record. Formalizing them yields a checked model of stationary search markets with threshold play, a checked reduction of the first best to a generalized assignment LP, and two graph lemmas (forest support of LP optima, the star-forest halving) that recur in rounding arguments for generalized assignment and budgeted allocation.

Difficulty

The first best is easy to reach once Proposition 4.4 linearizes it; the obstacle is incentives. Turning a first-best solution into an equilibrium by keeping its meeting rates fails, because agents raise or lower their thresholds relative to the pairwise thresholds the platform would choose, and constraint (6e) couples every type's threshold to all thresholds on the opposite side through $\max(\tau_m,\tau_w)$. The paper therefore has to control equilibrium thresholds without computing them, which it does only in star-shaped markets, and it needs a case analysis there (Case 1 and Subcases 2(a), 2(b) of Proposition 4.8) in which the meetings of the first best are sometimes discarded. Each of the reductions loses a factor: 2 in the passage from a forest to stars and 2 inside each star.

Formalization scope

The sides are separate finite types M and W with one law F m w per pair, serving both sides. The standing assumptions are $\delta>0$; $\alpha_\theta>0$ for every type; each $F_{mw}$ a probability measure with no atoms (NullSingletonClass, the paper's "continuous distribution"); and an integrable identity under each $F_{mw}$. The positivity of $\alpha_\theta$ and the integrability are added: the paper uses both implicitly. Tails are taken over $[a,\infty)$. LP feasibility includes $\beta\ge0$, which the paper leaves implicit; Lemma 4.6 also assumes nonnegative capacities. $\rho_{mw}$ is the supremum of $A$ over $[0,\infty)$, never defined as a fixed point.

"Approximation of the first-best optimum" is stated against every first-best feasible candidate, so no supremum appears. An induced stationary equilibrium always includes the best-response constraint (6e); a formalization that drops it, or that lets the equilibrium use pairwise thresholds, makes the goal compare the first best with itself and is ruled out. With an empty side both welfares vanish and the goal holds, as in the paper.

The "polynomial-time" part of Theorem 4.1 is not posed: the paper's computational model (oracle access to the laws, footnote 15) is not specified precisely enough to formalize. The source is the arXiv v2 preprint (18 Aug 2021); the Management Science version may number results differently. Proofs of any milestone, auxiliary lemmas about tail integrals of atomless laws, and LP vertex arguments are all welcome.

Selected references

• N. Immorlica, B. Lucier, V. Manshadi, A. Wei, Designing Approximately Optimal Search on Matching Platforms, Management Science, 2023; preprint arXiv:2102.09017v2. https://arxiv.org/abs/2102.09017
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46, 1990. https://doi.org/10.1007/BF01585745
• D. Chakrabarty, G. Goel, On the approximability of budgeted allocations and improved lower bounds for submodular welfare maximization and GAP, SIAM Journal on Computing 39(6), 2010. https://doi.org/10.1137/080735503
• S. Banerjee, S. Gollapudi, K. Kollias, K. Munagala, Segmenting two-sided markets, WWW 2017. https://doi.org/10.1145/3038912.3052578

Motivation

Every Bitcoin transaction recorded on the blockchain pays a fee, and the blockchain processes only a few transactions per second. The Lightning Network is a layer-two protocol that moves repeated payments off chain: two parties lock funds in a payment channel, exchange payments by updating the channel's balance, and touch the blockchain only to open, close or reset the channel. Whether a channel is worth opening is an economic question. Locked funds forgo interest, and a channel whose balance is exhausted must be reset on chain at a cost.

Guasoni, Huberman and Shikhelman (Management Science, 2023) model this trade-off with Poisson payment streams and continuous discounting, and obtain closed-form channel costs (their Theorem 1). Their Theorem 2 turns those costs into necessary conditions: a channel can be cheaper than settling every payment on chain only if the on-chain fee exceeds an explicit threshold depending on the reset cost, the payment rate and the interest rate. This mission formalizes Theorem 2, its two proofs, and the on-chain benchmark (Lemma 1) against which every channel is measured.

Setting

Node 1 pays node 2 one unit at the jumps of a Poisson process with rate $\lambda_1$, and node 2 pays node 1 at the jumps of an independent Poisson process with rate $\lambda_2$. The discount rate $r>0$ is the opportunity cost of capital per unit of time, $B$ is the cost of resetting a channel, and $C$ is the cost of one on-chain transaction. Node $i$ commits the amount $l_i$ to the channel.

On-chain settlement. If every payment of a stream with rate $\lambda$ is settled on chain, the expected discounted cost is $\mathbb E\big[\sum_{n\ge1}e^{-r\tau_n}C\big]=C\lambda/r$, where $\tau_n$ is the $n$-th arrival time (Lemma 1). Two streams of rate $\lambda$ cost $2C\lambda/r$.

Unidirectional channel. If only one node pays, at rate $\lambda$, a channel of size $m$ costs (Theorem 1(i), equation (1))

$$\mathrm{uniCost}(m)=m+B\Big(\big(\tfrac{r+\lambda}{\lambda}\big)^{m}-1\Big)^{-1}.$$

Bidirectional channel. With

$$\alpha_\pm=\frac{\lambda_1+\lambda_2+r\pm\sqrt{(\lambda_2-\lambda_1)^2+r^2+2r(\lambda_2+\lambda_1)}}{2\lambda_2}$$

(equation (4)), a channel with sizes $l_1,l_2$ costs $\mathrm{biCost}(l_1,l_2)$, the expression (3) in $\alpha_\pm^{l_1}$, $\alpha_\pm^{l_2}$ and $\alpha_\pm^{l_1+l_2}$. In the symmetric case $\lambda_1=\lambda_2=\lambda$ it simplifies, with $\alpha=\alpha_+$, to

$$l_1+l_2+\frac{B(\alpha^{l_1}+\alpha^{l_2})}{(\alpha^{l_1}-1)(\alpha^{l_2}-1)}.$$

A channel costs less than on-chain transactions if, for some size, its cost is strictly below the on-chain cost of the streams it carries.

Formalization targets

Goal: Theorem 2

For $B,r,\lambda>0$ and any fee $C$:

1. if $\mathrm{uniCost}(m)<\lambda C/r$ for some $m>0$, then

$$C>\log\Big(1+B\log\big(1+\tfrac r\lambda\big)\Big);\tag{5}$$

2. if $\mathrm{biCost}(l_1,l_2)<2C\lambda/r$ for some $l_1,l_2>0$ with $\lambda_1=\lambda_2=\lambda$, then

$$C>3\Big(\frac{B\kappa^4}{4}\Big)^{1/3}-\frac B{12}\kappa^2,\qquad \kappa=\log\frac{r+2\lambda+\sqrt{r(4\lambda+r)}}{2\lambda}.\tag{6}$$

Milestones

• Lemma 1: the on-chain cost $C\lambda/r$.
• Part (i) chain: the change of variable $\kappa=\log(1+r/\lambda)$ that turns the excess cost into $F(m)=C/(1-e^\kappa)+B/(e^{\kappa m}-1)+m$; the unique minimizer $\hat m=\cosh^{-1}(B\kappa/2+1)/\kappa$ and the minimum value; inequality (16); the sufficient condition (17)–(20) for on-chain settlement to be strictly cheaper; Theorem 2(i).
• Part (ii) chain: the symmetric cost and $\lambda/r=\alpha/(\alpha-1)^2$; the reduction (21) to equal sizes; the hyperbolic form and the bounds $1/x^2-1/3<\operatorname{csch}^2x<1/x^2$ of (22); the minimization (24) of the lower bound (23); Theorem 2(ii).
• Expansions: the right-hand sides of (5) and (6) equal $Br/\lambda+o(r)$ and $3(Br^2/(4\lambda^2))^{1/3}-Br/(12\lambda)+o(r)$ as $r\to0^+$.

Significance

Theorem 2 gives the qualitative conclusion of the paper in quantitative form: channels pay off only when on-chain fees are high, reset costs low, payment rates high, or interest rates low. Read as a contrapositive, it says that below the thresholds, settling on chain is at least as cheap for every channel size, so no optimization over sizes is needed to rule a channel out. The expansions show the two thresholds scale differently in the interest rate, linearly for a unidirectional channel and as $r^{2/3}$ for a symmetric bidirectional one. The paper's subsequent asymptotic results (Theorem 3) rely on the same reductions.

The theorem is proved in the paper; nothing here is open. To our knowledge none of it is formalized. A formalization adds a machine-checked verification of a proof that contains several informal steps: a minimizer of a two-variable function is assumed to exist, two inequalities are stated non-strictly where strict ones are needed, and one sentence states an "if and only if" with $\le$ where $<$ is meant. Lemma 1 also requires the discounted sum over a Poisson process to be integrable, which the paper's renewal argument takes for granted.

Difficulty

The bidirectional cost (3) is a ratio of differences of real powers of two algebraic numbers, and its minimum over two sizes has no closed form, so the threshold cannot be read off an explicit optimum. The paper replaces the optimum by reductions whose rigorous versions are the substance of the work: the passage from (3) to the symmetric form, the reduction of a two-variable minimization to the diagonal (asserted in the paper through a Hessian computation and the existence of a minimizer, neither of which is carried out), and a lower bound on $\operatorname{csch}^2$ that holds on all of $(0,\infty)$ and is not in Mathlib. The obvious approach of bounding the cost at its minimizer fails for the same reason it fails on paper: no minimizer is given. For part (i), the minimizer involves $\cosh^{-1}$, and the minimal value still depends on $C$ through two terms, so a condition on $C$ alone does not follow by rearrangement. Lemma 1 requires an exchange of expectation and infinite sum over a Poisson process, which the paper's renewal argument assumes.

Formalization scope

• Costs as closed forms for real sizes. uniCost and biCost are the paper's expressions (1) and (3) with real sizes and real powers (Real.rpow). Theorem 2's proofs minimize over real sizes, and the hypotheses quantify over real sizes, so the statements imply their versions for natural sizes. The probabilistic derivation of (1) and (3) from the balance random walk is the subject of the sibling mission Channels I.
• Explicit on-chain costs. The comparisons are with $\lambda C/r$ and $2C\lambda/r$, written out; there is no opaque on-chain cost function.
• Strict and existential. "Costs less" is strict and asserted for some size; the conclusions on $C$ are strict. No sign is imposed on $C$; $B,r,\lambda>0$.
• Lemma 1 uses the published definition QueueingFundamentals.Foundations.IsExpInterarrivals of i.i.d. exponential interarrival times; the conclusion asserts integrability as well as the value $C\lambda/r$.
• Corrections recorded in the statements. (17)–(20) is stated with the strict conclusion $F>0$ that (17) gives, for all $m>0$; (21) is stated in midpoint form, $H(m,m)\le H(l_1,l_2)$ for $m=(l_1+l_2)/2$, which requires no minimizer.
• Two different $\kappa$. In part (i) $\kappa=\log(1+r/\lambda)$; in part (ii) $\kappa=\log\alpha_+$. They are never identified.
• Asymptotics are little-o along $r\to0^+$ (𝓝[>] 0) with $B$ and $\lambda$ fixed.

Ruled out as trivializing: fixing $B$, $r$ or $\lambda$; restricting to natural sizes without saying so; an existentially chosen $\kappa$; weakening either strict inequality; or an on-chain cost under which the comparison is vacuous.

Needed infrastructure: real-power calculus and convexity on $(0,\infty)$, $\cosh^{-1}$ and $\sinh$ bounds, little-o expansions of $\log$ and $\cosh^{-1}$ near their base points, and the Laplace transform of Gamma laws for Lemma 1. The csch inequality (22) and Lemma 1 are reusable beyond this mission. Contributions to any milestone are welcome independently.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, published online Nov. 6, 2023, pp. 1–14. https://doi.org/10.1287/mnsc.2022.01664
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, technical report, 2016. https://lightning.network/lightning-network-paper.pdf
• G. Huberman, J. D. Leshno, C. Moallemi, Monopoly without a Monopolist: An Economic Analysis of the Bitcoin Payment System, Review of Economic Studies 88(6), 2021. https://doi.org/10.1093/restud/rdab014

Motivation

A firm that fills a fixed number of positions from a pool of applicants faces uncertainty at every stage: applicants differ in value, and an offer may be declined. When offers must go out at once, as in a recruiting season with a common deadline, the firm decides a single offer set and lives with however many candidates accept. Sending too few offers leaves positions empty; sending too many hires beyond capacity at a cost. This trade-off is the same as overbooking in revenue management (airline seats, hotel rooms), with the difference that candidates are heterogeneous in both value and acceptance probability.

Epstein and Ma (arXiv:2210.04059v3, Operations Research 2024) study three hiring-pipeline models through linear programming relaxations. This mission formalizes their lower bound for the third model, Simultaneous Offering (§3.3 and §6 of the paper). The question it answers is practical: how much is lost if the firm restricts itself to value-ordered policies, which send offers to the $m$ most valuable candidates for some $m$, instead of searching over all $2^n$ offer sets? Value-ordered policies are natural, because a firm rarely wants to withhold offers from its best candidates, and the optimal one is computable by a short dynamic program. The paper shows (Example 1, p. 25) that they can be arbitrarily bad in general, and that they are provably good when every candidate's value is bounded below.

Setting

An instance $I=(k,n,p,v)$ has $k$ positions and $n$ candidates, $1\le k\le n$. Candidate $i$ accepts an offer independently with probability $p_i\in[0,1]$ and then contributes value $v_i\ge0$. Candidates are labelled so that $v_1\ge v_2\ge\dots\ge v_n$. The firm chooses an offer set $S\subseteq[n]$; with $A\subseteq S$ the random set of acceptances, the reward is

$$\sum_{i\in A}v_i-\big[\,|A|-k\,\big]^+,$$

the cost per candidate hired beyond capacity being normalised to $1$. $\mathrm{OPT}_{\mathrm{sim}}(I)$ is the best expected reward over offer sets. For $\tau>0$ the instance is $\tau$-bounded, $I\in\mathcal I^\tau_{\mathrm{sim}}$, if $v_i\ge\tau$ for all $i$; the interesting range is $\tau\in(0,1)$, since for $\tau\ge1$ offering to everyone is optimal.

The benchmark is the LP relaxation

$$\mathrm{LP}_{\mathrm{sim}}(I)=\max_{y,z}\ \sum_{i}v_ip_iy_i+z\quad\text{s.t.}\quad z\le k-\sum_ip_iy_i,\ \ z\le0,\ \ 0\le y_i\le1,$$

which charges the overage cost on the expected number of hires. Write $V_{\mathrm{high}}=\{i:v_i>1\}$ and $P_{\mathrm{high}}=\sum_{i\in V_{\mathrm{high}}}p_i$.

The algorithm $\mathrm{ALG}^s_{\mathrm{sim}}$, for $s\in[0,1]$, takes an optimal LP solution $y$, scales its total mass $\sum_iy_ip_i$ by $s$ to $\kappa$, and fills mass $\kappa$ from the most valuable candidate down: $y'_i=1$ while the prefix mass $\sum_{l\le i}p_l$ stays at most $\kappa$, one fractional entry, then zeros. Offers are then sent independently with probabilities $y'_i$, so the algorithm randomises between two value-ordered policies. Its expected reward is $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)$.

The guarantee involves the truncated Poisson mean $\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]=\sum_{j\ge0}\min\{j,k\}e^{-\lambda}\lambda^j/j!$ and

$$\alpha^\tau_k=\sup_{0\le s\le1}\Big(s-\frac{s}{\tau}+\frac{\mathbb E[\min\{\mathrm{Pois}(sk),k\}]}{\tau k}\Big).$$

Formalization targets

Goal: Theorem 3 (p. 30)

For $\tau\in(0,1)$, every $I\in\mathcal I^\tau_{\mathrm{sim}}$, every optimal solution of $\mathrm{LP}_{\mathrm{sim}}(I)$ and a maximiser $s^*\in[0,1]$ of the objective defining $\alpha^\tau_k$,

$$R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}(I)\ \ge\ \alpha^\tau_k\,\mathrm{LP}_{\mathrm{sim}}(I).$$

Milestones

• Lemma 10 (p. 27): $\mathrm{LP}_{\mathrm{sim}}(I)\ge\mathrm{OPT}_{\mathrm{sim}}(I)$.
• Lemma 11 (p. 27): some optimal LP solution is a filled prefix $y=(1,\dots,1,y_j,0,\dots,0)$ with $y_j>0$.
• Lemma 12 (p. 28): the total mass of such a solution is $P_{\mathrm{high}}$ if $P_{\mathrm{high}}>k$ and $\min\{k,P_{\mathrm{total}}\}$ otherwise (posed under the disclosed hypothesis $v_i>0$, $v_i\ne1$, $p_i>0$).
• Monotonicity (App. D.5, p. ec16): $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ is decreasing in $x$.
• Proposition EC.2 (p. ec3): $\mathbb E[\min\{\mathrm{Pois}(k),k\}]=k(1-e^{-k}k^k/k!)$.
• Lemma 13 (p. 29): if $P_{\mathrm{high}}\le k$, then $R_{\mathrm{ALG}^s_{\mathrm{sim}}}(I)\ge\big(s-s/\tau+\mathbb E[\min\{\mathrm{Pois}(sk),k\}]/(\tau k)\big)\mathrm{LP}_{\mathrm{sim}}(I)$ for every $s\in[0,1]$.
• The $\mathrm{ALG}^1$ bound (p. 30): on every $\tau$-bounded instance, $R_{\mathrm{ALG}^1_{\mathrm{sim}}}(I)\ge(1-e^{-k}k^k/(k!\tau))\,\mathrm{LP}_{\mathrm{sim}}(I)$.
• Lemma 14 (p. 29): if $P_{\mathrm{high}}>k$, deflating the acceptance probabilities to an instance with $P_{\mathrm{high}}=k$ does not increase the ratio $R_{\mathrm{ALG}^{s^*}_{\mathrm{sim}}}/\mathrm{LP}_{\mathrm{sim}}$ (posed under the disclosed hypothesis $v_i\ne1$).

Significance

Theorem 3 makes value-ordered policies an $\alpha^\tau_k$-approximation on $\tau$-bounded instances, through Lemma 10. The factor tends to $1$ as $k\to\infty$ for fixed $\tau$: at $s=1$ it is at least $1-e^{-k}k^k/(k!\tau)=1-O(1/\sqrt k)$ (Corollary 4). The paper's Theorem 4, the subject of the companion mission in this series, shows that no value-ordered policy beats the same expression with the supremum over $s\ge0$, so the analysis is tight wherever the two suprema coincide. The interpretation of $\tau$ is how soft the capacity is: the bound degrades exactly as the overage cost dominates candidate values.

The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it has been machine-checked. A complete development would give the platform an overbooking-type stochastic selection model with an exact expected reward, an LP benchmark, and the truncated-Poisson constant that recurs in prophet-inequality and online-matching analyses (the $k$-uniform correlation gap of Yan 2011). Proposition EC.2 and the monotonicity of $\mathbb E[\min\{\mathrm{Pois}(x),k\}]/x$ are reusable on their own.

Difficulty

The obvious argument compares the algorithm's random number of hires with the LP's expected number and loses everything to the overage term: the LP pays $[\mathbb E|A|-k]^+$, the algorithm pays $\mathbb E[|A|-k]^+$, and Jensen's inequality points the wrong way. The gap must be controlled by a sum of independent Bernoulli variables against a Poisson variable of the same mean, uniformly over how the mass is spread across candidates. A second difficulty is the regime $P_{\mathrm{high}}>k$, where the LP optimum deliberately exceeds capacity; a direct bound there does not reduce to the first case, and the paper's reduction (Lemma 14) changes the instance rather than the algorithm. Tie cases $v_i=1$ make the LP optimum non-unique, which the formal statements must handle explicitly.

Formalization scope

Candidates are Fin n (0-based), all quantities are real. The sorted labelling $v_1\ge\dots\ge v_n$ is part of instance validity (Antitone I.v), as the paper assumes after relabelling; ties may be ordered arbitrarily. Every expectation is an explicit finite sum over the $2^n$ hire sets with independent probabilities $y'_ip_i$; there is no measure theory. The truncated Poisson mean is the series of the Poisson pmf. $\mathrm{LP}_{\mathrm{sim}}(I)$ is the supremum of the objective over the feasible set, which is the LP value; $\alpha^\tau_k$ is the supremum over $[0,1]$. $s^*$ is any maximiser of the $\alpha^\tau_k$ objective over $[0,1]$; one exists by continuity. A candidate with $p_i=0$ receives $y'_i=0$, which changes no reward.

The algorithm's reward is the exact expected reward of the run with independent offers, never the bound produced in the paper's proof, and the comparison is with the LP value at an optimal solution, not with the objective at an arbitrary feasible point; $\alpha^\tau_k$ is the supremum of the specific Poisson expression, not a free constant.

Two statements carry disclosed hypotheses, because the printed versions fail at ties: Lemma 12 assumes $v_i>0$, $v_i\ne1$, $p_i>0$, and Lemma 14 assumes $v_i\ne1$. Counterexamples are in the items' Formalization Notes. Theorem 3 and Lemma 13 need neither and hold for every optimal LP solution.

A complete development needs Poisson series manipulations (the closed form, concavity of $\lambda\mapsto\mathbb E[\min\{\mathrm{Pois}(\lambda),k\}]$), a Bernoulli-to-Poisson comparison for $\mathbb E\min\{\sum_iD_i,k\}$, and fractional-knapsack structure for the LP. Contributions of alternative proofs of any milestone, and of the Poisson facts as standalone results, are welcome.

Selected references

• B. Epstein, W. Ma, Selection and Ordering Policies for Hiring Pipelines via Linear Programming, arXiv:2210.04059v3 (2023); Operations Research (2024). https://arxiv.org/abs/2210.04059
• Q. Yan, Mechanism Design via Correlation Gap, Proceedings of SODA 2011, 710–719. https://doi.org/10.1137/1.9781611973082.56
• M. T. Goodrich, R. Tamassia, Algorithm Design: Foundations, Analysis, and Internet Examples, Wiley, 2001, Chapter 5 (fractional knapsack).

Motivation

Optimal stopping with partial information sits between two classical problems. In the secretary problem a decision maker sees values in random order, knows nothing about how they are generated, and must stop on the best one; the optimal guarantee is $1/e$. In the i.i.d. prophet inequality the values are independent draws from a known distribution, and the best guarantee, relative to the expected maximum, is the constant $\alpha^*\approx 0.745$: Hill and Kertz (1982) and Kertz (1986) showed that no stopping rule does better on every distribution, and Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld (2017, doi:10.1145/3033274.3085137) gave a rule that achieves it. Practical settings, such as pricing from historical data, lie in between: the distribution is unknown, but samples of it are available.

Correa, Cristi, Epstein and Soto (arXiv:2011.06516v2) interpolate between the two problems with the $p$-sample-driven optimal stopping problem: each of $N$ adversarial values is independently revealed in advance (a sample) with probability $p$, and the remaining values arrive online in random order. At $p=0$ this is the secretary problem; as $p\to1$ it approaches the i.i.d. prophet inequality. They show that the optimal competitive ratio $\alpha(p)$ of the limit problem is the value of an infinite-dimensional linear program, and they construct an explicit threshold rule whose guarantee $\tilde\alpha(p)$ is the root of a scalar equation.

Prior work on learning a distribution from samples obtained guarantees $\alpha^*-O(\varepsilon)$ with $O(n^2/\varepsilon)$ samples (Correa, Dütting, Fischer, Schewior, 2019) and with $O(n/\varepsilon^6)$ samples (Rubinstein, Wang, Weinberg, 2020). Theorem 9 of the paper, the goal of this mission, gives such a guarantee with $O(n/\varepsilon)$ samples.

Setting

Fix $p\in(0,1)$. The guarantee of the explicit threshold rule is the number $\tilde\alpha(p)\in(0,1)$ solving

$$\ln p+\frac{\tilde\alpha(1-p)^2}{p}=\sum_{i=1}^{\infty}\frac{\ln\bigl(1-\tilde\alpha+\tilde\alpha[(i+1)p^i-ip^{i+1}]\bigr)}{i(i+1)}.\tag{19}$$

Lemma 7 of the paper shows that (19) has exactly one root in $(0,1)$. The i.i.d. prophet constant $\alpha^*\in(0,1)$ is the solution of

$$\int_0^1\frac{dy}{y(1-\ln y)+1/\alpha^*-1}=1 .$$

The proof of Theorem 9 (Appendix B.9) works with three auxiliary functions of $p$, each depending on $\alpha^*$ as a parameter:

$$a(p)=\sum_{i\ge1}\frac{\ln\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)}{i(i+1)}+\alpha^*(2p-p^2),\qquad b(p)=\frac1{p^2}\sum_{i\ge1}\frac{1}{i(i+1)\bigl(\tfrac1p-\alpha^*(1-p^i(1+i(1-p)))\bigr)},$$ $$c(p)=\sum_{i\ge1}\frac{p^{i-1}-p^i}{\tfrac1{p\alpha^*}-1+p^i(1+i(1-p))}.$$

Appendix B.7 also names the two sides of (19): $f(p,\alpha)=\ln p+\alpha(1-p)^2/p$ and $g(p,\alpha)=\sum_{i\ge1}\ln(1+\alpha(p^i(1+i(1-p))-1))/(i(i+1))$. In Lean, IsAlphaTilde p a and IsAlphaStar s are shared predicates in SampleDrivenOS.Limit; aB9 s p, bB9 s p, cB9 s p, fB7 p α, and gB7 p α are in SampleDrivenOS.Linear.

Formalization targets

Goal: Theorem 9 (p. 17)

$$\text{for every }p\in(0,1):\qquad \tilde\alpha(p)\ \ge\ \alpha^*p .$$

It is stated for every root $\tilde\alpha$ of (19) and every solution $\alpha^*$ of the integral equation; neither existence nor uniqueness is assumed.

Milestones (Appendix B.7 and B.9, in the order the proof uses them)

1. B.7: $f(p,\cdot)$ is strictly increasing on $[0,1]$ and $g(p,\cdot)$ non-increasing on $[0,1)$.
2. B.9: if (19) holds with "$\le$" at $\alpha^*p$ in place of $\tilde\alpha$ (after the substitution $\tilde\alpha=f(p)p$), then $\tilde\alpha(p)\ge\alpha^*p$.
3. B.9: that inequality is equivalent to $\alpha^*\le a(p)$.
4. B.9: $a$ is differentiable on $(0,1)$ with $a'(p)=2\alpha^*(1-p)-b(p)+c(p)$, also in term-by-term form.
5. B.9: $b(p)\ge 1/p$.
6. B.9: $c(p)\le\frac1p\int_0^1\frac{dy}{1/(p\alpha^*)-1+y(1-p\ln y)}-\alpha^*(1-p)$.
7. B.9: using the defining equation of $\alpha^*$,

$$\frac1p\int_0^1\frac{dy}{\tfrac1{p\alpha^*}-1+y(1-p\ln y)}\le\frac1p-\frac{1-p}{p}\Bigl(\frac1{p\alpha^*}-\frac1e\Bigr)\ln\frac{\tfrac1{p\alpha^*}+\tfrac pe}{\tfrac1{p\alpha^*}+\tfrac pe-1}.$$

8. B.9: for all $s\in[0.74,0.75]$ and $p\in(0,1)$, $\bigl(\frac1{ps}-\frac1e\bigr)\ln\frac{1/(ps)+p/e}{1/(ps)+p/e-1}\ge0.8$.
9. B.9: if $\alpha^*\in[0.74,0.75]$, then $c(p)\le\frac1p-\alpha^*(1-p)(1+\frac1p)$.
10. B.9: under the same hypothesis, $\frac{d}{dp}a(p)\le0$ on $(0,1)$.

Significance

The explicit rule's guarantee $\tilde\alpha(p)$ is a lower bound on the optimal ratio $\alpha(p)$, and Theorem 8 (a separate mission of this series) shows $\tilde\alpha(p)\to\alpha^*$ as $p\to1$. Theorem 9 makes that convergence quantitative and uniform: the guarantee is at least linear in $p$, so with $p=1-\varepsilon$, an online set of size $n=\varepsilon N$ and $O(n/\varepsilon)$ samples the rule earns $\alpha^*-O(\varepsilon)$ of the expected maximum. This improves the sample complexity of the earlier learning-based results by a polynomial factor, in a model more general than theirs.

The theorem is proved in the paper; it has no machine-checked proof. The proof is elementary real analysis on explicit series and integrals, and one of its steps is a numerical check that the paper does not carry out in print. A formalization turns that numerical claim into a certified inequality and checks a chain of estimates in which one inequality sign is misprinted (see Formalization scope).

Difficulty

The statement is about two implicitly defined numbers. $\tilde\alpha(p)$ has no closed form, and $\alpha^*$ is defined by an integral equation. Evaluating both numerically at finitely many $p$ proves nothing for the remaining $p$, and the inequality is tight at $p=1$ ($\tilde\alpha(1)=\alpha^*$), so no uniform slack is available near $p=1$.

Concavity of $\tilde\alpha$ would give the result immediately, and the paper reports it numerically, but the authors were unable to prove it; the argument must avoid it. The remaining work handles infinite series whose terms depend on $p$ through both $p^i$ and $i(1-p)$: differentiating such a series term by term requires uniform control of the derivative series, comparing it with an integral needs a monotonicity argument, and one step needs a bound valid on an entire two-parameter region rather than at a point.

Formalization scope

• Numbers, not processes. No probability, program or algorithm appears in Lean. Everything is a real-valued function on $\mathbb R$.
• Predicates, not choice. $\tilde\alpha(p)$ and $\alpha^*$ enter as IsAlphaTilde p a (with $0<a<1$) and IsAlphaStar s (with $0<s<1$). Statements quantify over every solution. Both exist, so the goal is not vacuous: existence of $\tilde\alpha$ is Lemma 7 (posed in the second mission of this series), and existence and uniqueness of $\alpha^*=1/\beta^*$ are posed as CorreaThreshold.Adaptive.beta_star_existsUnique (512ff915-7ec1-4d24-87b3-bc8adfee6bad).
• Series. Every series is a Lean tsum over i : ℕ with the paper's index $i\ge1$ shifted to i + 1. For parameters in $(0,1)$ all series are summable, so tsum is the true sum; summability is part of what solvers prove, never a hypothesis. Differentiability of $a$ is likewise a conclusion (HasDerivAt), never assumed.
• Total functions. Real.log 0 = 0 makes the integrands' values at $y=0$ equal their limits, so the interval integrals are the true integrals. Every division ($1/p$, $1/(ps)$) is at a positive argument under the stated ranges, and every logarithm's argument is positive.
• $\alpha^*\approx0.745$. The paper uses this approximation through the interval $\alpha^*\in[0.74,0.75]$ of its numerical check. Milestones 9 and 10 carry that interval as a hypothesis; the goal does not. The lower bound $\alpha^*>0.745$ is posed as CorreaThreshold.Adaptive.inv_beta_star_gt (ce70487c-b155-4e47-9ce8-8348dc1b1645). The upper bound $\alpha^*\le0.75$ (numerically $\alpha^*\approx0.74544$) is posed nowhere and is welcome as a lemma.
• A printed slip. The paper prints the conclusion of milestone 9 as "$c(p)\ge\dots$". The surrounding argument requires and announces "$\le$", and the formal statement uses $\le$.
• Ruled-out trivializations. Fixing $p$, replacing $\alpha^*$ by the numeral $0.745$ (a weaker statement, since $0.745<\alpha^*$), stating $a$'s monotonicity through deriv (which is $0$ at non-differentiable points), or replacing $\tilde\alpha$ by a chosen value all change the theorem. None is used.
• Reusable infrastructure. Welcome contributions include term-by-term differentiation of tsums under a dominating series, Riemann-sum comparisons for monotone integrands, a Chebyshev-type integral inequality for two decreasing functions, and certified interval arithmetic for a two-variable inequality such as milestone 8.

Selected references

• J. Correa, A. Cristi, B. Epstein, J. A. Soto, Sample-Driven Optimal Stopping: From the Secretary Problem to the i.i.d. Prophet Inequality, arXiv:2011.06516v2, 2021 (journal version: Mathematics of Operations Research, 2024). https://arxiv.org/abs/2011.06516v2
• J. Correa, P. Foncea, R. Hoeksma, T. Oosterwijk, T. Vredeveld, Posted Price Mechanisms for a Random Stream of Customers, ACM EC 2017; Mathematics of Operations Research 46(4), 2021. https://doi.org/10.1145/3033274.3085137
• T. P. Hill, R. P. Kertz, Comparisons of stop rule and supremum expectations of i.i.d. random variables, Annals of Probability 10(2), 1982 (reference [26] of the paper). https://doi.org/10.1214/aop/1176993767
• R. P. Kertz, Stop rule and supremum expectations of i.i.d. random variables: a complete comparison by conjugate duality, Journal of Multivariate Analysis 19, 1986 (reference [28] of the paper).
• J. Correa, P. Dütting, F. Fischer, K. Schewior, Prophet Inequalities for I.I.D. Random Variables from an Unknown Distribution, ACM EC 2019. https://doi.org/10.1145/3328526.3329627
• A. Rubinstein, J. Z. Wang, S. M. Weinberg, Optimal Single-Choice Prophet Inequalities from Samples, ITCS 2020. https://doi.org/10.4230/LIPIcs.ITCS.2020.60