Formal verification complete: Theorem 2 and all 12 mission targets are Proved. The main theorem has 0 open proof dependencies, including the zero-multiplier case. These results apply to the formalized independent-box model described below. Paper: arXiv v3. The revised statement formalized here is intended for v4, which will be available on arXiv shortly.

Why study budgeted Pandora’s box?

An experiment can be valuable without being worth its price. In Bayesian optimization, a function evaluation may require training a model, running a simulation, or carrying out a laboratory experiment. The decision is therefore both where to evaluate and how much information to buy. A rule that responds only to relative costs can miss the effect of making every evaluation expensive.

Xie, Astudillo, Frazier, Scully, and Terenin connect this question to Pandora's box, a sequential search problem with independent hidden rewards. Their paper uses the exact solution of this simpler model to motivate an acquisition function for Bayesian optimization. This mission formalizes the author-revised version of the paper's fixed expected-budget result, Theorem 2, including its zero-multiplier boundary. Theorem 1, the classical cost-per-sample result attributed to Weitzman, is supporting material. Paper, Sections 2–3.

Independent boxes and a fixed expected budget

There are finitely many boxes in a nonempty set $X$. Box $i$ contains a real random reward $F_i$ with a known distribution and finite absolute first moment. The rewards are mutually independent. Opening it costs a deterministic amount $c_i>0$ and reveals its reward exactly.

A policy chooses a first box, then uses its observed history and independent randomization to choose an unopened box or stop. It must open at least one box, cannot reopen a box, and cannot resume after stopping. Its terminal reward is the largest observed reward. There is no outside option of zero. Define

$$R(\pi)=\mathbb E\!\left[\max_{i\text{ opened by }\pi}F_i\right],\qquad C(\pi)=\mathbb E\!\left[\sum_{i\text{ opened by }\pi}c_i\right].$$

For a fixed real budget $B$, feasibility means $C(\pi)\le B$. This is an expected-budget constraint; individual runs may exceed $B$. Write

$$R_B^*=\sup_{C(\pi)\le B}R(\pi),\qquad R_{\mathrm{all}}=\mathbb E[\max_{i\in X}F_i].$$

For $\lambda>0$, the reservation index $g_i(\lambda)$ is the unique finite solution of

$$\mathbb E[(F_i-g_i(\lambda))_+]=\lambda c_i.$$

At zero multiplier, the formalization defines

$$g_i(0)=\operatorname{ess\,sup}F_i\in\mathbb R\cup\{+\infty\}.$$

This is an explicit extension of the paper's positive-cost definition. A generalized Gittins policy first opens a maximal-index box. It subsequently opens a remaining maximal-index box when its index exceeds the incumbent, and stops when the incumbent exceeds every remaining index. Equality permits either action. Ties between boxes and stopping ties may be randomized. The zero branch is not defined by choosing an arbitrary root of the zero-level improvement equation. Original positive-cost rule, equation (5) and Section 3.2.

Formalization target: Theorem 2 with the zero boundary

Use the budget condition in the author-revised Theorem 2 supplied on 23 October 2026,

$$\min_i c_i<B.$$

There is no upper budget cap: the target includes $B\ge\sum_i c_i$, as well as budgets below that sum.

Define the dual envelope

$$A_B(\lambda)=\sup_\rho\{R(\rho)-\lambda C(\rho)\}+\lambda B.$$

The main target is the existence of $\lambda\ge0$ minimizing this envelope on $[0,\infty)$ and a generalized Gittins policy $\pi$ satisfying

$$\pi\in\arg\max_\rho\{R(\rho)-\lambda C(\rho)\},\qquad C(\pi)\le B,\qquad\lambda(B-C(\pi))=0,$$ $$\forall\rho,\quad C(\rho)\le B\Longrightarrow R(\rho)\le R(\pi).$$

Thus the policy is optimal for the fixed expected budget. Positive multipliers require exact expected expenditure; zero multipliers permit slack. No strict reward-gap assumption is imposed on this main target, and no continuity, atomlessness, or boundedness assumption is added to the reward laws.

Correction relative to arXiv v3. Theorem 2 in that version requires a strictly positive multiplier under the numerical budget bounds alone. That conclusion has a counterexample: independent rewards $F_1=1$, $F_2\sim\mathrm{Uniform}[0,2]$, unit costs, and $B=3/2$. Opening box 2 and then box 1 exactly when $F_2<1$ achieves $R_{\mathrm{all}}=5/4$ within budget, whereas every positive-multiplier index policy has strictly smaller reward. Lemma 9's inference that every zero-penalty optimum must open all boxes is invalid. The mission targets the author-revised statement, which allows zero multipliers and removes the upper budget bound, rather than the strict-positivity claim in arXiv v3. Source statement and proof, Appendix B.5.

Supporting targets include the reservation root; Theorem 1; exact-budget and complementary-slackness certificates; convexity and attainment of the dual minimum; joint expected-cost and expected-reward limits at positive multipliers; budget matching and Gittins cost extrema; a zero-multiplier policy-limit lemma; and a feasible zero-index policy when zero minimizes the dual. Some milestones isolate or strengthen steps used in the revised proof rather than reproducing a numbered statement verbatim. The corrected positivity result remains as a supporting corollary:

$$R_B^*<R_{\mathrm{all}}\quad\Longrightarrow\quad\text{every dual minimizer is strictly positive}.$$

What the verified result establishes

Budgeted Pandora’s box is motivated by a common feature of Bayesian optimization in practice: experiments, simulations, and model evaluations must be chosen within a limited resource budget. It asks how to choose evaluations sequentially to maximize the expected best observed reward, subject here to a bound on expected total cost. An optimal index policy for this problem provides a theoretical benchmark for budget-aware Bayesian optimization.

All 12 linked theorem targets have completed Lean proofs, including the zero-multiplier boundary and the supporting probability, policy-limit, and optimization results. The verified development establishes the author-revised expected-budget theorem and supplies reusable components for finite adaptive search and constrained optimization.

The empirical performance of the acquisition function and the extension to correlated Gaussian-process Bayesian optimization are outside the goal. No global Bayes-optimality claim is made for that correlated extension. Paper, Section 3.3.

Key steps in the formal argument

An optimal penalized policy need not meet a prescribed budget. Atoms and tied indices can make expenditure jump as the multiplier changes. The targets therefore include expected-cost extremes within the index-policy class and randomization that interpolates those costs.

At zero multiplier, finite reservation roots can escape to positive infinity. Arbitrary ties in the resulting extended indices need not respect the budget; the zero-dual-minimum milestone asserts existence of a feasible choice, rather than feasibility of all choices. Finite first moments must suffice throughout.

The convergence target records both expected reward and expected cost, including the slope needed in the envelope argument. The directional derivative of an affine objective uses its linear part; Lemma 13 in the author-revised manuscript includes this correction. Earlier proof in arXiv v3, before the revision, Appendices B.5–B.6.

Formalization scope and conventions

The Lean model uses $n+1$ boxes, integrable Borel probability laws on $\mathbb R$, their product measure, and an independent uniform seed on $[0,1]$. Measurable policies observe ordered padded histories. Finite recursion enforces irreversible stopping and distinct openings. Terminal maxima start at the first observation, not zero.

Expectations are Bochner integrals; their integrability and the boundedness of real policy suprema are established from the model in the verified supporting lemmas. Zero indices use EReal and the infimum of almost-sure upper bounds. Index conditions apply to all valid histories, including histories of probability zero. Negative multipliers are excluded by the generalized-rule definition. The strict-gap predicate is used only for the positivity corollary.

Definitions contain no proof placeholders. All twelve linked targets have status Proved, and the main theorem has zero open proof dependencies. Verification was performed by Prove2Me's server using Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474.

Selected references

The paper is available as arXiv v3. The revised statement formalized here is intended for v4, which will be available on arXiv shortly.

• Qian Xie, Raul Astudillo, Peter I. Frazier, Ziv Scully, Alexander Terenin. Cost-aware Bayesian Optimization via the Pandora's Box Gittins Index. NeurIPS 2024. arXiv v3, 16 January 2025; proceedings.
• Martin L. Weitzman. Optimal Search for the Best Alternative. Econometrica 47(3), 1979, pp. 641–654. DOI.