Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
We present a general necessary and sufficient criterion for the possibility of a state transformation from one mixed Gaussian state to another of a bi-partite continuous-variable system with two modes. The class of operations that will be considered is the set of local Gaussian completely positive trace-preserving maps.
This mission is the statement-level formalization of Conditions for the local manipulation of Gaussian states (arXiv:quant-ph/0109126v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2: exact LOG conversion criterion (Proposition 2, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
In this paper we give several equivalent formulations of the additivity conjecture for constrained channels, which formally is substantially stronger than the unconstrained additivity. To this end a characteristic property of the optimal ensemble for such a channel is derived, generalizing the maximal distance property. It is shown that the additivity conjecture for constrained channels holds true for certain nontrivial classes of channels. Recently P. Shor showed that conjectured additivity properties for several quantum information quantities are in fact equivalent. After giving an algebraic formulation for the Shor's channel extension, its main asymptotic property is proved. It is then used to show that additivity for two constrained channels can be reduced to the same problem for unconstrained channels, and hence, "global" additivity for channels with arbitrary constraints is equivalent to additivity without constraints.
This mission is the statement-level formalization of On Shor's channel extension and constrained channels (arXiv:quant-ph/0306196v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2: constrained versus asymptotic extension additivity (Theorem 2: constrained versus asymptotic extension additivity, PDF p. 13). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
The trade-off capacity region of a quantum channel characterizes the optimal net rates at which a sender can communicate classical, quantum, and entangled bits to a receiver by exploiting many independent uses of the channel, along with the help of the same resources. Similarly, one can consider a trade-off capacity region when the noiseless resources are public, private, and secret key bits. In [Phys. Rev. Lett. 108, 140501 (2012)], we identified these trade-off rate regions for the pure-loss bosonic channel and proved that they are optimal provided that a longstanding minimum output entropy conjecture is true. Additionally, we showed that the performance gains of a trade-off coding strategy when compared to a time-sharing strategy can be quite significant. In the present paper, we provide detailed derivations of the results announced there, and we extend the application of these ideas to thermalizing and amplifying bosonic channels. We also derive a "rule of thumb" for trade-off coding, which determines how to allocate photons in a coding strategy if a large mean photon number is available at the channel input. Our results on the amplifying bosonic channel also apply to the "Unruh channel" considered in the context of relativistic quantum information theory.
This mission is the statement-level formalization of Quantum trade-off coding for bosonic communication (arXiv:1105.0119v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Thermal entropy: convergent power series (Lemma 4: thermal entropy power series, PDF p. 7). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
17 results of the paper are not stated yet, because the library lacks an interface they need:
The hypothesis testing problem of two quantum states is treated. We show a new inequality between the error of the first kind and the second kind, which complements the result of Hiai and Petz to establish the quantum version of Stein's lemma. The inequality is also used to show a bound on the first kind error when the power exponent for the second kind error exceeds the quantum relative entropy, and the bound yields the strong converse in the quantum hypothesis testing. Finally, we discuss the relation between the bound and the power exponent derived by Han and Kobayashi in the classical hypothesis testing.
This mission is the statement-level formalization of Strong Converse and Stein's Lemma in the Quantum Hypothesis Testing (arXiv:quant-ph/9906090v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum Stein lemma at every fixed positive error (§3, Theorem 2, (10): quantum Stein lemma, corrected positive-error domain, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We consider quantum channels with one sender and two receivers, used in several different ways for the simultaneous transmission of independent messages. We begin by extending the technique of superposition coding to quantum channels with a classical input to give a general achievable region. We also give outer bounds to the capacity regions for various special cases from the classical literature and prove that superposition coding is optimal for a class of channels. We then consider extensions of superposition coding for channels with a quantum input, where some of the messages transmitted are quantum instead of classical, in the sense that the parties establish bipartite or tripartite GHZ entanglement. We conclude by using state merging to give achievable rates for establishing bipartite entanglement between different pairs of parties with the assistance of free classical communication.
This mission is the statement-level formalization of Quantum broadcast channels (arXiv:quant-ph/0603098v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 and its explicit nonregularization limitation (seed paper result) (Theorem 1 and its explicit nonregularization limitation (seed paper result), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
5 results of the paper are not stated yet, because the library lacks an interface they need:
Quantum channels can be described via a unitary coupling of system and environment, followed by a trace over the environment state space. Taking the trace instead over the system state space produces a different mapping which we call the conjugate channel. We explore the properties of conjugate channels and describe several different methods of construction. In general, conjugate channels map M_d to M_d' with d < d', and different constructions may differ by conjugation with a partial isometry. We show that a channel and its conjugate have the same minimal output entropy and maximal output p-norm. It then follows that the additivity and multiplicativity conjectures for these measures of optimal output purity hold for a product of channels if and only if they also hold for the product of their conjugates. This allows us to reduce these conjectures to the special case of maps taking M_d to M_d' with a minimal representation of dimension at most d. We find explicit expressions for the conjugates for a number of well-known examples, including entanglement-breaking channels, unital qubit channels, the depolarizing channel, and a subclass of random unitary channels. For the entanglement-breaking channels, channels this yields a new class of channels for which additivity and multiplicativity of optimal output purity can be established. For random unitary channels using the generalized Pauli matrices, we obtain a new formulation of the multiplicativity conjecture. The conjugate of the completely noisy channel plays a special role and suggests a mechanism for using noise to transmit information.
This mission is the statement-level formalization of Properties of Conjugate Channels with Applications to Additivity and Multiplicativity (arXiv:quant-ph/0509126v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
30 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity (Theorem 5 / paper headline: conjugation preserves multiplicativity and entropy additivity, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
17 results of the paper are not stated yet, because the library lacks an interface they need:
It has been observed by numerous authors that a quantum system being entangled with another one limits its possible entanglement with a third system: this has been dubbed the "monogamous nature of entanglement". In this paper we present a simple identity which captures the trade-off between entanglement and classical correlation, which can be used to derive rigorous monogamy relations. We also prove various other trade-offs of a monogamy nature for other entanglement measures and secret and total correlation measures.
This mission is the statement-level formalization of Monogamy of entanglement and other correlations (arXiv:quant-ph/0310037v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1, Eqs. (2)–(3): complementarity of entanglement and classical correlation (Theorem 1, Eqs. (2)–(3): complementarity of entanglement and classical correlation, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
1 results of the paper are not stated yet, because the library lacks an interface they need:
We show the equivalence of two different notions of quantum channel capacity: that which uses the entanglement fidelity as its criterion of success in transmission, and that which uses the minimum fidelity of pure states in a subspace of the input Hilbert space as its criterion. As a corollary, any source with entropy rate less than the capacity may be transmitted with high entanglement fidelity. We also show that a restricted class of encodings is sufficient to transmit any quantum source which may be transmitted on a given channel. This enables us to simplify a known upper bound for the channel capacity. It also enables us to show that the availability of an auxiliary classical channel from encoder to decoder does not increase the quantum capacity.
This mission is the statement-level formalization of On Quantum Fidelities and Channel Capacities (arXiv:quant-ph/9809010v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
23 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement and minimum-subspace capacities coincide (Abstract; Theorem 1 and Corollary 1, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
A longstanding open problem in quantum information theory is to find the classical capacity of an optical communication link, modeled as a Gaussian bosonic channel. It has been conjectured that this capacity is achieved by a random coding of coherent states using an isotropic Gaussian distribution in phase space. We show that proving a Gaussian minimum entropy conjecture for a quantum-limited amplifier is actually sufficient to confirm this capacity conjecture, and we provide a strong argument towards this proof by exploiting a connection between quantum entanglement and majorization theory.
This mission is the statement-level formalization of Majorization theory approach to the Gaussian channel minimum entropy conjecture (arXiv:1111.1986v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Single-use reduction: C1 iff C2 iff C3; C4 is sufficient (C1–C4; Appendix 1, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
We present an efficient family of quantum circuits for a fundamental primitive in quantum information theory, the Schur transform. The Schur transform on n d-dimensional quantum systems is a transform between a standard computational basis to a labelling related to the representation theory of the symmetric and unitary groups. If we desire to implement the Schur transform to an accuracy of epsilon, then our circuit construction uses a number of gates which is polynomial in n, d and log(1/epsilon). The important insights we use to perform this construction are the selection of the appropriate subgroup adapted basis and the Wigner-Eckart theorem. Our efficient circuit construction renders numerous protocols in quantum information theory computationally tractable and is an important new efficient quantum circuit family which goes significantly beyond the standard paradigm of the quantum Fourier transform.
This mission is the statement-level formalization of The Quantum Schur Transform: I. Efficient Qudit Circuits (arXiv:quant-ph/0601001v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite Gelfand–Zetlin labels fit in binary registers (III B: finite GZ labels and binary storage, PDF p. 11). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
8 results of the paper are not stated yet, because the library lacks an interface they need:
Characterizing genuine multipartite quantum correlations in quantum physical systems has historically been a challenging problem in quantum information theory. More recently however, the total correlation or multipartite information measure has been helpful in accomplishing this goal, especially with the multipartite symmetric quantum (MSQ) discord [Piani et al., Phys. Rev. Lett. 100, 090502, 2008] and the conditional entanglement of multipartite information (CEMI) [Yang et al., Phys. Rev. Lett. 101, 140501, 2008]. Here we apply a recent and significant improvement of strong subadditivity of quantum entropy [Fawzi and Renner, arXiv:1410.0664] in order to develop these quantities further. In particular, we prove that the MSQ discord is nearly equal to zero if and only if the multipartite state for which it is evaluated is approximately locally recoverable after performing measurements on each of its systems. Furthermore, we prove that the CEMI is a faithful entanglement measure, i.e., it vanishes if and only if the multipartite state for which it is evaluated is a fully separable state. Along the way we provide an operational interpretation of the MSQ discord in terms of the partial state distribution protocol, which in turn, as a special case, gives an interpretation for the original discord quantity. Finally, we prove an inequality that could potentially improve upon the Fawzi-Renner inequality in the multipartite context, but it remains an open question to determine whether this is so.
This mission is the statement-level formalization of Multipartite quantum correlations and local recoverability (arXiv:1412.0333v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §2, (2.1); §3: local recoverability from the multipartite information gap (§2, (2.1); §3: local recoverability from the multipartite information gap, PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Majority vote is a basic method for amplifying correct outcomes that is widely used in computer science and beyond. While it can amplify the correctness of a quantum device with classical output, the analogous procedure for quantum output is not known. We introduce quantum majority vote as the following task: given a product state where each qubit is in one of two orthogonal states or , output the majority state. We show that an optimal algorithm for this problem achieves worst-case fidelity of . Under the promise that at least of the input qubits are in the majority state, the fidelity increases to and approaches as increases. We also consider the more general problem of computing any symmetric and equivariant Boolean function in an unknown quantum basis, and show that a generalization of our quantum majority vote algorithm is optimal for this task. The optimal parameters for the generalized algorithm and its worst-case fidelity can be determined by a simple linear program of size . The time complexity of the algorithm is where is the number of input qubits.
This mission is the statement-level formalization of Quantum majority vote (arXiv:2211.11729v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
61 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Quantum majority vote: Theorem 1.2 (Quantum majority vote: Theorem 1.2, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
3 results of the paper are not stated yet, because the library lacks an interface they need:
Machine-learned models of molecular energies and properties are trained on the output of quantum-chemistry calculations, and a common way to make them data-efficient is to build the physical symmetries of the problem into the architecture. When the input is not a point cloud but a set of matrices expressed in an atomic-orbital basis (Fock, density, overlap and Hamiltonian matrices from a cheap mean-field calculation), the relevant symmetry is the freedom to rotate the orbital basis of each atom independently: a rotation of the molecule, or any other unitary change of the local frames, changes every matrix element but not the physics.
Qiao, Christensen, Welborn, Manby, Anandkumar and Miller (arXiv:2105.14655v4, published in PNAS 2022) introduce UNiTE (Unitary N-body Tensor Equivariant network), the architecture behind OrbNet-Equi. They state as eq. (4), p. 3, that the network must satisfy for every isometric basis rotation , and prove this property in Appendix S2.6 (pp. 26–28) for a generalized version of the network: tensors of any order , complex scalars, and an arbitrary unitary change of basis on each atom. The empirical results of the paper (QM9, MD17, GMTKN55) rest on this design principle, but the mathematical content of the paper is the equivariance proof.
There are atoms . Atom carries a finite basis , and the concatenated basis is the set of pairs . An N-body tensor of order is a function of concatenated indices; its sub-tensor at collects the entries whose -th index lies in atom .
A group (the paper's ; in the experiments) acts through unitary representations , and each atom has a subgroup . An element with acts on tensors by the local action (S26):
The network's hidden features assign to each label of a unitary representation and each channel a vector ; acts by . Matching matrices relate the atomic basis to a basis adapted to the decomposition .
The UNiTE network (Methods 1.1; Appendix S2.5) consists of:
Under the hypotheses the paper's proof uses — compatibility (S35) of the matching matrices, the Clebsch–Gordan property (S33) of , equivariance (S32) of the diagonal reduction, invariance of the attention weights, and positivity of the EvNorm constants — for every , tensor and atom ,
The proof in S2.6 rests on three results of S2.4 and four labelled sub-proofs:
The theorem is what justifies feeding UNiTE features in arbitrary local frames: the predicted invariant quantities (energies) do not depend on the choice of atomic-orbital phases or orientations. The vector-valued outputs, such as dipole moments, then transform correctly. Without it, the model would have to learn the symmetry from data or from augmentation. The same argument applies to other architectures acting on matrices in local bases, for example models of Hamiltonian or density matrices.
The result is proved in the paper, with a proof written at the level of index manipulations. To our knowledge it has no machine-checked proof. Formalizing it pins down exactly which hypotheses each layer needs: (S35) on the matching matrices, the complex conjugate in (S36), the intertwining form of (S33), and invariance of the attention weights. It also yields a reusable library of statements about tensor-product and block-diagonal actions of unitary representations. Theorem S1 for an arbitrary group with a complete catalogue of irreducibles is a statement of independent interest: finite-dimensional unitary representations are completely reducible, which Mathlib does not yet provide outside finite groups.
No single step is deep; the difficulty is bookkeeping across dependent index types. The local action is block-diagonal over atoms, so cross-atom terms must be shown to vanish. Sub-tensor indices are dependent on the atom sequence . The block convolution's cancellation uses unitarity and the conjugate. The reverse matching layer needs the adjoint form of (S35), which uses that is a subgroup (closed under inverses). The point-wise block reindexes a double sum through a Kronecker product. The full network is a two-phase recursion whose attention weights depend on the current features, so the induction must carry the equivariance of every intermediate feature. Theorem S1 needs complete reducibility of a finite-dimensional unitary representation of an arbitrary group, together with the identification of each irreducible summand with a catalogue member.
A tempting shortcut, assuming each layer equivariant and composing, proves nothing about UNiTE: the content is that these specific layers are equivariant under these specific hypotheses.
All scalars are complex; the paper's real (orthogonal) case is the special case of real unitary matrices. is replaced by an abstract group ([Group K]), representations are homomorphisms K →* Matrix.unitaryGroup ι ℂ, and the catalogue of irreducibles of is a family with the hypothesis CatalogComplete (every irreducible unitary representation is equivalent to some ), the formal reading of the paper's "we have abstracted the labelling details … into the index L". The subgroups are S u : Subgroup K, and every hypothesis is assumed only for .
Committed conventions:
Σ u, ι u;Trivializing formalizations are ruled out. The layers are defined concretely, not replaced by maps assumed equivariant. The action is local, one unitary per atom, not one global unitary. The complex conjugate in (S36) is kept. Irreducibility of the catalogue and its completeness are both stated in Theorem S1 and the corollaries.
The development needs one definitions module (OrbNetEqui.Equivariance.Basic) and Mathlib's matrices, unitary groups, block-diagonal and Kronecker matrices. Contributions are welcome on every milestone; the building-block lemmas (block-diagonal and Kronecker actions of unitary matrices, unitary invariance of the regularized norm) and complete reducibility of finite-dimensional unitary representations are reusable beyond this mission.
Forecast aggregation asks how to combine several experts' probability forecasts for the same event into one forecast. The two classical answers are linear pooling (average the probability vectors) and logarithmic pooling (average the log-probabilities and renormalize). Neither is justified by the way forecasts are usually evaluated: with a proper scoring rule, a payment rule under which reporting one's true belief maximizes expected reward. Neyman and Roughgarden (arXiv:2102.07081, Operations Research 2023) tie the aggregation method to the scoring rule. For each proper scoring rule they define quasi-arithmetic (QA) pooling with respect to , which recovers linear pooling for the quadratic (Brier) score and logarithmic pooling for the log score, and they justify it in several ways. This mission formalizes the first justification, the paper's Theorem 4.1: QA pooling is the unique max-min optimal way for an agent paid by to aggregate the forecasts of experts it has sub-contracted.
The result places the paper in a line of work on scoring rules and convex analysis: the Savage representation of proper scoring rules as tangent planes of a convex function (Gneiting and Raftery, JASA 2007, Theorem 2), the link between entropy maximization and worst-case expected loss (Grünwald and Dawid, Annals of Statistics 2004), and the result of Chun and Shachter (UAI 2011) that, for outcomes, experts rewarded with the same scoring rule cannot be prevented from colluding profitably, by all reporting what Neyman and Roughgarden call the QA pool of their reports.
There are outcomes. A forecast is a point of the standard simplex , and is the vertex with a in coordinate . A scoring rule is a function : an expert who reports receives if outcome happens. The rule is proper if for every belief and every report ,
with equality only when . It is regular if is real except possibly when . The forecast domain is the set of at which every is real, and the expected reward function is . The paper assumes throughout that each and are continuous on .
An exposure function of satisfies the Savage representation
so is a subgradient of at . The Bregman divergence is .
Given forecasts and non-negative weights adding to , the QA pool is the unique at which is a subgradient of . An agent paid by who pays expert the amount and reports earns the profit
For a regular, proper, continuous scoring rule with exposure function , forecasts and weights adding to :
the minimum is attained at every with ; it is non-negative; and it is positive unless all reports with positive weight are equal. All four clauses are part of the goal.
In the order the paper's proof uses them:
Theorem 4.1 says that an agent who sub-contracts experts and is paid by the same proper scoring rule can guarantee itself the largest worst-case profit, uniformly over outcomes, by reporting the QA pool, and that no other report achieves this guarantee. It gives an operational reason to aggregate with the method the scoring rule induces rather than a fixed one, and the strict positivity of the guarantee unless the weighted experts agree recovers, as a special case, the two-outcome collusion result of Chun and Shachter. The same objects (QA pools, exposure functions, Bregman divergences of expected rewards) carry the paper's later results on learning expert weights online and on axiomatizing QA pooling.
The theorem is proved in the paper; none of it is machine-checked. The mission produces a Lean statement and proof of Theorem 4.1 in full generality, including boundary pools where some outcome has probability zero, together with reusable statements about proper scoring rules on the simplex that are not in Mathlib: the Savage representation, non-negativity of the expected-reward Bregman divergence, existence and uniqueness of QA pools, and first-order optimality conditions on the simplex.
When lies in the interior of and is differentiable, first-order optimality gives directly, and the rest is algebra. The difficulty is the boundary. The QA pool can have for some ; need not be differentiable there; and for rules such as the logarithmic score at points with , so 's subgradients may blow up near the boundary of . Showing that the pool avoids the points where is (Claim 3.10) and that the multipliers exist with the right sign there requires the continuity of into the extended reals, not just convexity of . Uniqueness of the maximizer also needs the strictness built into properness.
Forecasts are functions Fin n → ℝ, and is Mathlib's stdSimplex ℝ (Fin n). The scoring rule takes values in EReal; only its values on matter, the expected score uses , and inner products are finite sums. Properness is strict, belief first and report second. is the real part of the expected score and is only evaluated on . Subgradients are taken relative to , the domain of . The exposure function is real-valued and constrained by the Savage representation on only; on it is determined up to a multiple of , and no statement depends on that choice. The Bregman divergence uses the exposure function in place of a gradient, since need not be differentiable at boundary forecasts. Continuity of is in the order topology of the extended reals. The QA pool is a predicate (a point of with the subgradient property), and its existence and uniqueness is a separate milestone. The profit is when the agent's report scores , and is an infimum over the outcomes.
A trivial formalization is ruled out: the QA-pool hypothesis of the goal is satisfiable (milestone 3), exposure functions exist (milestone 1), and the continuity assumptions of the paper are kept as hypotheses rather than dropped.
Not formalized: the paper's results on learning expert weights (Theorems 5.1, 5.3), its axiomatizations (Theorems 6.6, C.7), which rules have convex exposure (Appendix D), the "if" direction of Proposition 3.1, and the second bullet of Proposition 3.4. Contributions of general lemmas on convex functions on the simplex (one-sided directional derivatives, first-order conditions at boundary minimizers) are welcome alongside the milestones.
A company that is about to launch a product often has several candidate versions of it (designs, packagings, feature bundles) and wants to know which one consumers like best. A common way to find out is to ask: show an arriving consumer a few versions and record which one they pick. Each such query costs time and money, and consumer answers are noisy, so the question is how to choose what to show, and when to stop asking, so that the most preferred version is found with a prescribed reliability using as few consumers as possible.
Y. Feng, R. Caldentey and C. T. Ryan, Robust Learning of Consumer Preferences (SSRN 3215614; Operations Research, doi:10.1287/opre.2021.2157), treat this as a sequential hypothesis test in the style of best-arm identification (Garivier and Kaufmann, 2016; Kaufmann, Cappé and Garivier, 2016). The difference from a bandit is in the feedback: an action is a set of versions, and an observation is a choice from that set drawn from an unknown choice model. The paper asks for a policy that is good not for one choice model but uniformly over a large nonparametric class of them, and shows that a simple likelihood-based policy achieves this.
There are versions, . A display set is a subset with ; is the collection of display sets. A preference gives, for each and , the probability that a consumer shown picks . A ranking is a permutation of , rank being the top.
For , the class of -separable preferences (Definition 1) consists of the with exactly for , , and a ranking such that within every display set, iff (for ), and moreover whenever . The goal is to identify the top-ranked version .
An admissible policy chooses, after each history , a distribution over display sets for the next consumer; it stops at a stopping time and selects . It is -accurate if for every it stops almost surely and ; a family is accurate if each is -accurate (Definition 2).
With and , Chernoff's information is
where is the set of preferences in with a different top-ranked version. The ordinal attraction (OA) preferences are , where is the rank of within .
The Myopic Tracking Policy (MTP, Algorithm 1) with threshold fits the OA ranking of maximum likelihood to the votes so far, stops when the generalized log-likelihood ratio against every OA ranking with a different top reaches , and otherwise shows the top- versions of the fitted ranking with probability , an explicit distribution given in (7).
There is a threshold such that
that is, for every choice of the initial display set the family is accurate and its worst-case rate is at most that of every accurate family. The goal states the shape of the result and does not fix the optimal value.
The theorem says that one fixed, computable policy is optimal against the hardest consumer population in a nonparametric class, without knowing the population. Its display rule is static and sparse: only the nested sets of top-ranked versions are ever shown. The value gives a closed-form benchmark for the number of consumers any reliable test must survey, and Proposition 2 shows it barely depends on . The lower bound (Theorem 1) is a change-of-measure argument that applies beyond this model, for example to identifying the top- versions or the full ranking.
The results are proved in the paper; none is formalized. A formalization would produce a reusable discrete framework for sequential testing with set-valued actions and categorical feedback (finite-history laws, stopping times, expected stopping times in ), a formal treatment of Chernoff-type max-min information over a choice-model class, and a machine-checked LP duality certificate for the optimal display distribution. It would also pin down the exact hypotheses: two printed statements need correction (see Formalization scope).
The class is infinite and nonparametric, so the usual best-arm identification arguments, which track an estimate of the true instance, do not apply directly: MTP only ever estimates within the OA family, even when the truth is not OA. The upper bound must show that the drift of MTP's log-likelihood process under an arbitrary is at least , which rests on the dominance structure of Lemmas 4–5 and on the optimality of the fixed distribution . The accuracy proof must control the error probability uniformly over with a threshold independent of and . Computing on OA preferences reduces to a linear program over all rankings with a different top, whose explicit primal and dual solutions require the identities of Lemmas 6–9.
Everything is finite or discrete and no measure theory is used. Versions are Fin K and rankings are Equiv.Perm (Fin K) with 0-based ranks (rank 0 is the top); the restricted rank stays 1-based. A preference is a function DS K → Fin K → ℝ. A policy is given by its display rule (a function of the history into ℝ≥0∞), a stopping predicate on histories, and a selection function; the law of a history is the explicit product , in , and , and all rates are in . Limits as are along 𝓝[>] 0. MTP's uniform tie-break enters as a mixture in the display rule; for stopping and selection do not depend on it.
Added hypotheses and readings, each disclosed in the items: (A-3) is required for only (as printed it is unsatisfiable at ); and ; ; (Algorithm 1's input); the initial display set is arbitrary. Theorem 1's first inequality is stated for , since it fails for close to . Theorem 6's final sentence (equality for OA preferences) is not formalized, since it fails for bounded thresholds. The constants of Lemma 10 and Theorem 7 are quantified after and before .
Trivializing formalizations are ruled out: Definition 1 is non-vacuous (an OA preference is shown to lie in ), the alternative sets require membership in , top-rankedness is tied to the (A-3) ranking, and the goal includes the accuracy of MTP. Without it, a tiny threshold would stop after one vote.
Not in scope: Theorem 2 (a different policy for finite classes), Propositions 1 and 3–7, Corollaries 2–3, and the numerical study. Contributions to any milestone are welcome. The finite-history probability layer and the lower-bound argument are reusable for other sequential identification problems.
Data marketplaces buy personal data from many individuals to estimate population statistics. Two features set such pricing apart from an ordinary procurement auction. First, each data owner has a private cost of sharing, so the buyer must design a menu of payments that elicits these costs truthfully. Second, data are correlated across people: an individual who refuses to share still loses privacy when similar people share. Liao, Su, Ziani, Wierman and Huang call the consequence the privacy paradox: privacy-conscious people may join a platform because abstaining does not protect them (arXiv:2105.14262, §1; published in Mathematics of Operations Research, 2024).
The paper asks how an analyst with a fixed budget should design such a mechanism when the goal is statistical: to estimate a population mean while trading off the bias caused by non-participants against the variance caused by sampling only some participants. The answer extends the optimal-auction framework of Myerson (Math. Oper. Res. 1981) and the data-procurement mechanisms of Roth and Schoenebeck (EC 2012) and Chen, Immorlica, Lucier, Syrgkanis and Ziani (EC 2018) to a setting with participation externalities and an adversarial correlation between data and costs.
Agents are split into groups . An agent in group has a cost drawn from a density on the support , with distribution function . At a fixed desired participation profile the privacy cost of a participant is with , a non-participant suffers , the gap is strictly increasing, and participants receive a benefit .
The analyst posts a menu: a selection probability and a payment for a reported cost . A participant with true cost who reports has expected utility
The menu is truthful if reporting maximizes this utility. An agent joins if some report gives utility at least , and the menu induces if the fraction of joining agents of group is for a threshold . The virtual cost is
For the statistical problem, Appendix C of the paper discretizes the costs and sorts all virtual costs of participants as , with cell probabilities summing to . Given agents, a budget , a constant collecting the participation terms, and a weight on the variance, the analyst chooses and an adversary chooses the data probabilities in the min-max program
subject to the budget , under the standing condition .
There are constants , , and a feasible, non-increasing allocation
such that for every feasible . The constants are left existential, as in the printed theorem; the case analysis that identifies them belongs to the milestones.
Theorem 1 is a participation-aware version of Myerson's characterization: it shows that the analyst loses nothing by restricting to monotone allocation rules with one explicit payment, and it pins down the payment that realizes a target participation rate. Theorem 2 then solves the analyst's worst-case bias–variance problem: the optimal selection probability is flat for cheap agents and decays like the inverse square root of the virtual cost for expensive ones. This shape explains when the mechanism can be strictly truthful (a strictly decreasing rule, Corollary 2, in the low-budget regime) and when only weak truthfulness is possible (a flat region, larger budgets).
The paper proves Theorem 2 for discrete costs and passes to continuous costs by letting the number of cells grow without bound, a step it asserts without proof. The mission formalizes the discrete theorem that Appendix C actually proves, together with both directions of Theorem 1. None of these results has a machine-checked proof yet.
The goal is a min-max statement about a program that is convex in the allocation and concave in the adversary's choice, with a coupled budget constraint. The natural first idea, to solve each player's first-order conditions and plug them into each other, does not by itself produce a solution: the analyst's best response clips at 1, the adversary's best response may be interior on some cells and at the boundary on others, and which cells are which depends on the budget. The paper resolves this by a case analysis on the ratio against the values of , with thresholds obtained from intermediate-value arguments, and each case requires its own multiplier and its own adversary strategy.
For Theorem 1 the obstacle is that the paper's envelope argument differentiates the allocation rule, while the theorem quantifies over all monotone rules, which need not be differentiable. The "only if" direction must be recovered from the convexity of the maximal utility as a function of the true cost.
All statements live in the namespace PrivacyParadox.Alloc and use one definitions file. The group layer fixes one desired profile, so , , and are functions of the cost or numbers; their dependence on participation rates and correlation strengths plays no role in Theorems 1–2. The discrete layer indexes cells by as the paper does, with real-valued data and Real.sqrt.
The formalization commits to the following conventions, each disclosed in the item it affects:
Two trivializing readings are excluded: the goal compares with every feasible allocation, so it is not the best-response property of Lemma 3, and it asserts the existence of rather than assuming an optimizer of the stated form.
A complete development needs elementary real analysis (interval integrals of monotone functions, Fubini on a triangle, the intermediate value theorem) and finite-dimensional convex optimization (first-order optimality for a concave quadratic on a box and for a separable convex program with one linear constraint). The latter two are reusable well beyond this mission. Proofs of milestones are welcome in any order. The continuous form of Theorem 2, Lemma 1 (the derivation of the objective from the Horvitz–Thompson estimator), Propositions 1–2 and Properties 1–4 are not part of the mission.
Many large-population systems are modelled as aggregative games: each agent's cost depends on its own decision and on an average of everybody's decisions. Examples are electric-vehicle charging and demand response, where a household's cost depends on its own consumption profile and on the aggregate load through the electricity price, and congestion and routing, where a traveller's cost depends on the total flow on the links used. In these applications individual decisions are often non-convex: a charging profile may be on/off, a route is a discrete choice, an appliance runs in fixed blocks. Without convexity, the classical existence theorems for pure Nash equilibria (Rosen 1965, Debreu–Glicksberg–Fan) do not apply, and a pure Nash equilibrium may fail to exist.
The intuition that "non-convexity averages out when many small agents are aggregated" goes back to Starr's work on markets with non-convex preferences (1969), based on the Shapley–Folkman lemma. Liu, Oudjane and Wan (arXiv:2011.12604, Mathematics of Operations Research) make it quantitative for sum-aggregative games: they show that a non-convex aggregative game with players has an approximate pure Nash equilibrium whose error decays like , and they construct it from an equilibrium of a convexified game.
There are players . Player chooses an action in a compact, nonempty, possibly non-convex set , of diameter at most . Write for its convex hull. There are matrices with spectral norm , . The cost of player at a profile is
where is defined on and is a neighbourhood of the set of aggregates with .
Assumption 1 requires that (1) is lower semicontinuous on for every , and (2) is -Hölder on uniformly in : , with .
For , an -pure Nash equilibrium (-PNE) is a feasible profile such that no player can lower its cost by more than through a unilateral deviation: for all and .
The convexified game has action sets and costs
with the probability simplex in : is the convex envelope of . A generator is the set of points carrying positive weight in a minimizer of this infimum. A point satisfies the -stability condition with respect to generators if for all and .
Under Assumption 1, with
the non-convex game has an -PNE. More precisely, if is a pure Nash equilibrium of and are arbitrary generators, every profile
is an -PNE of . Both sentences are part of the goal.
If is only an -PNE of and satisfies the -stability condition with respect to a generator profile, the same disaggregation is an -PNE of with .
In attack order: Lemma 5.1 (a fixed point of the argmin map of a function continuous in , jointly lower semicontinuous and convex in ); Theorem 5.3 (existence of a PNE in games with convex compact action sets, convex lower semicontinuous costs and uniform equicontinuity in the other players' actions); Lemma 5.5 (1)–(2), (3) and (4) (properties of the convex envelope and of generators); Proposition 2.3 (the convexified game has a PNE); the Shapley–Folkman lemma (Lemma 5.4, first bullet, already proved on the platform); Starr's bound (Lemma 5.4, second bullet); Lemma 5.6 (1) ( at generator points); Theorem 2.7.
The result. Proposition 2.4 gives existence of approximate pure equilibria in a class of games where exact pure equilibria need not exist, with an explicit error bound that vanishes as the population grows, for fixed aggregate dimension . It also says how to obtain one: solve the convexified game, which is a convex game with lower semicontinuous costs, and round its equilibrium to generator points. Theorem 2.7 makes the construction robust to approximate solutions of the convexified game, which is what an iterative algorithm delivers. The paper's later sections (a randomized disaggregation and an application to flexible electricity consumption) rest on these two statements.
Formalizing it. The results are proved in the paper; none of them is formalized. The Shapley–Folkman lemma itself is proved on the platform and is reused here. The mission adds a quantitative Starr bound in Euclidean norm, an existence theorem for pure equilibria under lower semicontinuity (an extension of Rosen's theorem that the authors prove themselves because they found no reference), the basic theory of the -point convex envelope, and the disaggregation argument. Formalization also checks the paper's statements: the printed definition of a generator, read literally, makes Theorem 2.7 false (see Formalization scope).
The disaggregation step needs more than "average over many players". The convexified equilibrium gives each player a point in , but the deviation analysis has to happen in the original game, at points of . Two facts must be combined: the generator points of a best response of are best responses of against the convexified profile, and a profile of generator points can be found whose aggregate is within of the convexified aggregate. The first fails if a generator is allowed to contain points of zero weight. The second fails with the naive bound: picking arbitrary generator points for the at most exceptional players of the Shapley–Folkman lemma gives an error of order , not ; the bound requires a choice that exploits Euclidean geometry.
On the existence side, Rosen's theorem does not apply to : is convex and lower semicontinuous in the own action, but it need not be continuous even when is (the paper gives a three-dimensional example on p. 5).
is EuclideanSpace ℝ (Fin d) and players are Fin n. A matrix is a continuous linear map from to ; its operator norm is the spectral norm of the paper. Deviations are Function.update x i y, and inside is evaluated at the profile in which player plays , so the aggregate contains . One -PNE predicate, parameterized by action sets and costs, serves both and . Hölder powers are real powers, and is not assumed. is a neighbourhood of the aggregate set of , encoded with nhdsSet. The infimum defining is a real infimum; at every profile of its set is nonempty and bounded below, so Lean's default value for empty or unbounded sets is never reached.
Three readings differ from the printed text, and each is the one the paper's proofs use. (i) A generator is the set of components with positive weight, as in the paper's Lemma 5.7; keeping zero-weight components makes Lemma 5.6, Theorem 2.7 and Proposition 2.4 false (a two-player example with exists). (ii) Lemma 5.5 (2), printed "for all ", is stated on , as its proof and Definition 2.2 require. (iii) Action sets are assumed nonempty. Lemma 5.1 is stated in any finite-dimensional real normed space; the uniform equicontinuity of Theorem 5.3 measures closeness coordinatewise, an equivalent norm. Starr's bound is stated with any upper bound on the diameters, which is equivalent to the maximal diameter.
A trivializing formalization is ruled out: is an infimum over representations of the player's own action, not over all points, so equilibria of are not arbitrary profiles; a sorry-free sanity check confirms that the definitions are satisfiable and agree with on a singleton action set.
Out of scope: Theorem 3.3, Propositions 2.8, 3.2, 3.4, Lemmas 2.6, 3.1, 5.6 (2), 5.7, 5.8, the full stability condition, mixed strategies, and the numerical study of §4. Contributions welcome: proofs of the milestones, in particular a reusable Starr bound and a reusable existence theorem for lower semicontinuous convex games.
In bundle size pricing (BSP) a seller of many products offers a menu of bundles in which the price of a bundle depends only on its size, the number of items in it. Customers choose which items to put in a bundle and which size to buy. Season tickets for theatres and sports teams, cable-TV channel packages and streaming plans priced by the number of simultaneous devices are priced this way, and BSP is known to recover much of the profit of full mixed bundling with only a handful of prices (Chu, Leslie and Sorensen 2011).
Choosing the optimal size prices is hard. For given prices, the customer's value for the best bundle of size is a maximal partial sum of order statistics of the item valuations, and the seller's expected profit depends on the joint law of these sums across sizes. Even when that law is known, it is not known whether the resulting pricing problem is tractable.
Li, Sun and Teo (2021) replace the exact choice model by the cross moment model (CMM) of Mishra, Natarajan, Tao and Teo (2012): only the mean vector and the covariance matrix of the bundle valuations are specified, and choice probabilities are those of the extremal distribution, among all laws with these two moments, that maximizes the customer's expected surplus. Their main result (Theorem 2) is that the seller's profit, written as a function of the choice probabilities, is concave, so the pricing problem becomes a concave maximization over a simplex. This mission formalizes that result.
Let be the number of bundle sizes. Let be the mean valuation vector, the vector of bundle costs, and the covariance matrix of the bundle valuations (the outside option, with value , is excluded). Write for the all-ones vector. The simplex and its interior are
A point is a vector of choice probabilities: is the probability that the size- bundle is bought, and the probability of buying nothing.
For a positive semidefinite matrix , denotes its unique positive semidefinite square root, and means that is positive semidefinite. Define
where is the diagonal matrix with diagonal , and below is the vector of diagonal entries of . In the paper, Theorem 1 and Lemmas 1–2 show that for every is the CMM demand at exactly one price vector, namely with
Substituting this price into the profit gives the BSP-CMM profit of Problem (6):
The statement is uniform in , , and in the positive definite ; it fixes no constant.
Concavity of turns bundle size pricing under the cross moment model into a concave program over the simplex: a local maximizer is global, and the problem can be passed to a conic solver through the semidefinite representation of milestone 5. The paper uses this to price bundles directly from two moments of the valuation distribution, and notes that the same reduction approximately solves other bundle pricing problems once they are written as multidimensional pricing problems. Before this result it was known that CMM choice probabilities are computable by convex optimization (Ahipaşaoğlu, Li and Natarajan 2018), but not whether pricing under CMM is tractable.
The result is proved in the paper; it has no machine-checked proof. The mission produces a formal statement of Theorem 2 against the explicit function (6), and the chain of the paper's proof as separately provable milestones. Several of these are reusable beyond the paper: Loewner concavity of , Loewner concavity of the square root composed with it, and the Schur-complement description of a bordered linear matrix inequality over the reals.
The function is not a composition of standard concave functions: it contains the inverse square root of a matrix that depends quadratically on , inside both a diagonal extraction and a quadratic form. The scalar composition rules for concavity do not apply to matrix-valued maps, and the second derivative of has no usable closed form. What is needed is the operator monotonicity and operator concavity of the matrix square root on positive semidefinite matrices (Horn and Johnson 1990). Mathlib has the corresponding results only for elements of C⋆-algebras, through the continuous functional calculus; real symmetric matrices with the Loewner order are a separate instance whose square root, monotonicity and concavity must be connected to that theory or proved directly.
Everything is stated inside BSPConvex.CMM. Vectors are Fin m → ℝ and matrices Matrix (Fin m) (Fin m) ℝ; is named Sig. The objects , , , , , , (defined by the displayed formula), (written literally as (6)), and the bordered matrix are definitions in one file. is CFC.sqrt under open scoped MatrixOrder, and is (A - B).PosSemidef throughout. is (CFC.sqrt (T q))⁻¹, the matrix inverse.
The formalization departs from the page in three disclosed ways:
A formalization that defines through or so that concavity is definitional, or that states the theorem on a set where it is vacuous, does not count: is the literal expression (6), and is nonempty for every (it contains ).
Contributions welcome beyond the milestones: a real-matrix version of operator monotonicity and concavity of the square root, the Schur complement criterion for real block matrices with a positive definite block, and differentiability of on positive definite matrices.
An online retailer decides, for every arriving customer, how to frame its catalog: which products are displayed, in which section or position, and at which of several price points. Framing changes demand. A product on a promotional banner sells more than the same product further down the page. The retailer must also decide which fulfillment center (FC) ships each order, and shipping costs depend on the distance from the FC to the customer. With limited inventory in each FC, framing and fulfillment interact: showing a product to a far-away customer can drain the stock that a closer, cheaper future order would have used.
Lei, Jasin, Uichanco and Vakhutinsky (SSRN 3282019; Manufacturing & Service Operations Management, 2021, doi:10.1287/msom.2021.1012) model this as the joint framing and fulfillment (JFF) problem. Customers choose by the multinomial logit (MNL) model. The paper builds the Randomized Framing and Fulfillment (RFF) policy from a deterministic relaxation, and proves that its relative loss against the optimal policy vanishes at rate as the market is scaled by . The work was carried out with data from a major U.S. retailer: 56 products in 27 FCs (§6).
There are products, customer regions, FCs and framing groups; group can hold at most products, and group means "not displayed". A framing assignment is a map . The feasible ones form
In each of periods at most one customer arrives, from region with probability . Product in group has attraction for , with , and price . A region- customer who sees buys with probability . The order is shipped from an FC that holds the product, at cost , and FC starts with units. is the optimal expected total profit (OPT').
The deterministic counterpart DET' replaces the 0/1 framing by fractions , with
Here
DET' maximizes , and its value is .
ConstrDist turns a fractional framing of one region into a distribution over , in three steps:
RFF runs ConstrDist on an optimal DET' solution for every region and period. Each period it samples , hides out-of-stock products, samples an FC with probability proportional to , and ships from , or from the cheapest FC with stock if is empty. The scaled problem has horizon and inventories ; its values are , and .
There are and such that for all , every optimal DET' solution and every choice of decompositions in ConstrDist,
and DET' has an optimal solution. Moreover, if , then for large and
The constants depend on the instance only.
The result shows that a policy computed once from a deterministic program loses only in absolute terms, despite three complications:
Lemma 3 is the reusable part. For MNL demand, any fractional framing can be realized exactly in expectation, for purchase probabilities and revenues simultaneously, by a randomization over feasible assignments. This makes fluid-based policies available for display, ranking and pricing decisions alike.
Status. The statement is published, but its printed proof is incomplete. EC 2 bounds RFF by a variant that ignores stock-outs and asserts that RFF "will generate zero profit" at a stock-out. RFF does not do that: it hides the product or re-routes the order, which changes all later inventories. The step is not justified. The statement was checked at planning by exact dynamic programming on four small instances, up to ; stayed between and . A complete proof, formal or informal, is new. None of these results has a machine-checked proof.
The obvious argument compares RFF with its deterministic plan period by period. Lemma 3 makes the expected sales and revenues match the plan exactly, and the total deviation of sales from plan is . That argument controls a policy that never runs out of stock. RFF does run out: after a stock-out it hides products and re-routes orders. So its later inventory, and hence its later framings and costs, differ from the plan in a path-dependent way. The difficulty is to bound the profit lost through this feedback by , uniformly over every optimal DET' solution, including time-varying ones, and every decomposition. A second, smaller difficulty is that DET' is not a linear program in . Lemma 5 and stationarity both need its reformulation as one.
Fin types; the no-display group is the last index. The standing assumptions are bundled in one predicate:
Fast-fashion chains and flash-sale sites rotate their assortments: a product is on display for a short window and is then replaced. Retailers that do this face a choice that a classical assortment model cannot express. They can show the whole catalog at once, or they can conceal part of it and reveal products one at a time. In the classical discrete-choice models, which include multinomial logit, nested logit and Markov chain choice, each consumer buys at most one product, so the order in which products are revealed is immaterial.
Ferreira and Goh (HBS Working Paper 17-041; published in Management Science, 2021, doi:10.1287/mnsc.2020.3610) let consumers buy several products. Each additional purchase is worth less to the consumer than the previous one. This diminishing marginal utility goes back to Marshall and appears in the satiation model of Baucells and Sarin (2007). With it, the order of revelation matters, and the paper asks whether concealment pays.
A retailer has products with nonnegative prices . A consumer has a random valuation shock for each product . The shocks are mutually independent, continuous and integrable random variables on a probability space . The quantity is the price-adjusted valuation of product . Buying a set of products gives the consumer the utility
where the marginal utility is nonnegative and decreasing.
In Lean a product is a pair (price, realized shock). seqRev v L k is the sequential revenue of a list L for a consumer starting with k purchases, fixedRev v L' is (4) along a list L', and ERsStar, ERfStar are the two optima.
Let be an optimized fixed assortment, and let be the revenue of the sequential assortment showing the same products in decreasing order of prices. Then
Part (b) fixes no constants and asserts only the sign of the value of concealment, which can be zero (Theorem 2 of the paper).
The result. Theorem 1 says that concealment never hurts a retailer facing multi-purchase consumers with diminishing marginal utility. Part (a) also gives a concrete policy, independent of the shock distributions: take the optimal fixed assortment and reveal its products from the most to the least expensive. The paper reads the gain as structural: the retailer learns nothing from offering products sequentially, yet it still gains from them. The rest of the paper builds on it. Theorem 2 characterizes when the value of concealment is zero, Theorem 3 gives its asymptotics, and §6 measures the decreasing-price heuristic numerically.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. The mission produces a reusable model of a multi-purchase consumer under fixed and sequential presentation, together with its basic monotonicity facts (Lemma 2, Remark 1). The goal is also stated pathwise, which is stronger than the paper's "with probability 1".
The obvious approach compares the two strategies product by product, and it fails. Under the fixed assortment the purchase decision for a product depends on its rank among the realized price-adjusted valuations. Under the sequential assortment it depends on the number of earlier purchases, which in turn depends on every earlier shock. Neither revenue is monotone in the order of presentation. Swapping two adjacent products can raise or lower the revenue, depending on the realization and on which of the two is more expensive. Lemma 4 identifies the one swap whose sign is controlled, and Lemma 2 bounds how far an extra purchase can shift the remaining revenue. The difficulty is to arrange swaps of this kind into a sorting of the decreasing-price sequence into a Definition-1 order, and to keep the bookkeeping exact when prices or valuations tie.
Trivializing encodings are ruled out: is the positional formula (4), not the sequential revenue in -order. Restricting to the products of the fixed assortment, or to the full set, would change the claim and is not done.
The development needs only finite sums, lists and permutations from Mathlib, plus Bochner integrals of bounded random variables. The list-level lemmas about seqRev (Lemmas 2 and 4, Remark 1) apply to any sequential-purchase model with diminishing marginal utility. Contributions are welcome on every milestone, and on general list-sorting lemmas that carry an interchange argument from adjacent swaps to a full permutation.
Not formalized here: Lemma 3 and Corollaries 1–2 (optimal sequences under hazard-rate and IFR conditions), Theorems 2–3, the forward-looking consumer model of §5, and the numerical study of §6.
A firm launching a new product (a drug, a software package, a digital download) must choose a price before it has data on its demand curve. Classical monopoly pricing needs the whole demand curve: the optimal price balances marginal revenue against marginal cost, and both depend on the curve's shape. Cohen, Perakis and Pindyck (Management Science; accepted version SSRN 2673810) ask how well a firm can do when it knows only two numbers: its constant marginal cost and the maximum price , the price at which consumers stop buying. Their answer is a rule that needs nothing else: charge the price that would be optimal if demand were linear through . They give closed-form performance guarantees for this rule under several demand families. The guarantee that holds for an entire nonparametric class is the one for concave inverse demand, and that is the subject of this mission.
The setting matters in practice when the firm need not plan output in advance (zero or near-zero marginal cost, no capacity decision): then the only decision is the price, and the slope of the demand curve, which determines how much will be sold, is immaterial for choosing it.
A market consists of
Selling units at the market-clearing price earns the profit . A firm that knew would choose an optimal quantity maximizing on , charge the optimal price , and earn .
The demand at price is , the quantity sold when the firm charges .
If demand were linear, with , the profit would be maximized at , at the price
which does not depend on . This is the linear price. The linear pricing rule charges whatever the true demand is, and earns .
In Lean these objects are Market, Market.Standing, profit, IsOptQty, linPrice, demandAt and linProfit in the namespace LinearPriceRule.Concave.
If is concave on , then an optimal quantity exists, , and every optimal quantity satisfies
Proposition 5 is a distribution-free guarantee: across the whole class of concave inverse demands, which contains linear, concave quadratic and many other shapes, a rule that uses only and loses at most half of the optimal profit. The rectangle shows that the factor cannot be improved within the class. Theorem 1 says in which direction the rule errs, under-pricing for concave and over-pricing for convex inverse demand, so a firm with qualitative information about curvature knows which way to adjust. The paper's parametric results (quadratic, monomial, semi-log, log-log demand) and its welfare comparisons are built on the same model.
The results are proved in the paper. As far as is known, none of them has been formalized. This mission provides a machine-checked model of a monopolist facing an unknown inverse demand on a bounded quantity interval, which other robust-pricing statements can reuse, together with the paper's argument for the concave case, carried out without the differentiability its Taylor-expansion proof of Theorem 1 assumes.
The paper's proof of Theorem 1 writes , equates marginal revenue with marginal cost, and applies a second-order Taylor expansion. None of this is available for the statement as formalized: is only continuous and concave, it may have kinks (the rectangle has one at ), and the optimum may sit at the corner , where the first-order condition fails. A proof must compare the profit at with profits at other quantities using only the defining inequality of concavity.
The second subtlety is the demand , a supremum over a set. Identifying with the profit of an actual quantity, and with , needs continuity and the optimality of : a flat stretch of at the optimal price would otherwise let exceed .
The convex half of Theorem 1 is false at a corner optimum. For on and , the optimum is with . That milestone therefore assumes .
Only Mathlib's convexity and order-theoretic infrastructure (ConcaveOn, ConvexOn, AntitoneOn, sSup on ℝ, the extreme value theorem on compact intervals) is needed. Proofs of the milestones are welcome in any order. The parametric Propositions 1–4, the welfare results (Propositions 6–7) and the uncertain- analysis of §3 are outside this mission.
In a spread betting market a market maker quotes a line for a quantity whose outcome is not yet known (a point spread in sports, a price level in finance), and bettors wager on either side of it. The market maker earns a commission on every bet and would like her line to sit at the median of , where both sides are equally likely and she carries no directional risk. She does not know the median: she must learn it from the bets themselves. Some bettors are informed: they know the median, and they can bet many times. An informed bettor who sees that the market maker learns from bets has an incentive to bluff, betting against his information to push the line the wrong way and then profiting from the mispriced line later.
Birge, Feng, Keskin and Schultz (SSRN 3283392, published in Operations Research, 2021, doi:10.1287/opre.2021.2109) show that natural Bayesian pricing policies are exploited in this way (their Theorem 1: non-converging lines and regret linear in the horizon) and design an inertial policy that is not. This mission formalizes the positive half of the paper: under the inertial policy the informed bettor's best response is an honest threshold strategy, the line converges to the correct median, and the market maker's regret grows only logarithmically.
The outcome is with unknown median , , and noise with c.d.f. . Under hypothesis the median is and has c.d.f. ; write and for the density. Assumption 1 requires the noise density to be continuously differentiable, symmetric around zero, and strictly positive on . The commission rate is .
Bets arrive one at a time. The market maker quotes ; a bet is (on ) or (on ). The winner is paid , the loser pays . At each bet the informed bettor chooses an action , possibly at random and based on the public history and his own past actions; is a bet, and leaves the bet to a myopic bettor, who bets with probability . The informed bettor's expected payoffs per bet are and , his total expected profit over bets is , and a best response maximizes when this is bounded, and otherwise. The market maker's regret is
her loss relative to a market maker who knows the median, and against best-responding bettors.
The inertial policy tracks the net bet count () and quotes . With , a residual probability sequence fixes through and (Proposition 2). The paper's choice is
The informed bettor's candidate best response is the threshold strategy , , with , and the admissible range of is with the explicit of (G.2)–(G.4). Write .
For every , and :
The first clause is (T3:2) of Theorem 3; it is part of the goal because the probability in Theorem 4 is defined by the best response.
In proof order: Proposition 2 (residual-probability representation); Lemma 4 (a discrete Dynkin formula); Lemmas G.1 and G.2 (properties of and of ); Lemma L.1 (a product-series test); Lemma L.2 (occupation sums); Lemmas 1–3 (the value function : finiteness, continuation profit, Bellman equation); Theorem 3 (bounded profit, threshold best response); Lemma 5 (regret as an additive functional ); Lemma H.1 ( is slowly vanishing and regular); Lemma L.4; Proposition K.2 (the general slowly vanishing case); Proposition 3 (rates for and ).
The result shows that a market maker facing a strategic, informed, repeat bettor can still learn: a policy that moves its line only gradually removes the incentive to bluff, so the informed bettor bets honestly when the line is far from his median and abstains otherwise. The line then converges to the truth almost surely, and the cost of learning is , against for Bayesian policies in the same market. Proposition K.2 extends the analysis to every slowly vanishing and generic threshold, which explains the choice : decaying faster makes the market state recurrent, slower makes the regret larger.
The results are proved in the paper; none of them has a machine-checked proof. A formalization checks a long chain of exact computations (closed-form solutions of birth–death difference equations, a Bellman verification over history-dependent strategies) whose constants and boundary cases are easy to get wrong. Lemma 4, Lemma L.1 and Lemma L.2 are general facts about Markov chains and product series, usable outside this model.
The market state is a birth–death chain whose drift vanishes: under , for large it moves up with probability . It is transient only because decays no faster than , and it grows like , so large-deviation arguments, which need the drift to dominate the noise, do not apply. The paper instead evaluates every quantity exactly through difference equations. The best-response claim is harder still: it must hold against every history-dependent randomized strategy, including bluffing ones, and the Bellman equation alone does not imply optimality for a total-reward criterion (every constant shift of a solution is a solution); finiteness and nonnegativity of and the identification of the threshold strategy's actual profit with are needed as well.
All statements live in the namespace SpreadBetting.Inertial. A structure Market bundles and the noise density , and Market.Standing collects the model's ranges, the fact that is a probability density, and Assumption 1. The c.d.f. is , and is the generalized inverse , certified by Proposition 2. Residual probabilities are functions used at and extended to by (E.1).
Expectations are exact finite recursions over bet histories, not integrals. A strategy maps the list of past (bet, own action) pairs and the current state to a probability vector over actions. The market state is a function of the public history and determines . The best response (2.3) ranges over all such admissible strategies, and its liminfs and suprema are taken in EReal. Almost-sure statements use the path law of the market-state chain on , from the published GittinsIndex definition (BanditAlgorithm.markovChainMeasure; coordinate is ). is the paper's Definition 1; "diverges at rate " means divergence to together with the bound.
The threshold , the bound and the policy are explicit, so none of the statements is trivially true. In particular, the goal does not take as a free strategy pinned by hypotheses, does not use a junk value for an infinite liminf, and does not restrict deviations to Markov strategies. Added hypotheses are disclosed item by item: on Lemma 1, whose proof uses it, and measurability and integrability on Lemma 4.
Contributions are welcome at every level: the general Lemma 4 and Lemma L.1, the difference-equation lemmas (L.2, L.4), the properties of and , and the Bellman verification of Theorem 3. A proof of the goal needs Borel–Cantelli or a transience criterion for birth–death chains on the path space, Mathlib's Ionescu–Tulcea construction, and elementary real analysis for the asymptotics of products .
Retailers and platforms increasingly set prices and choose which products to display per customer, using observed customer attributes (location, device, purchase history). The decision rule is usually built in two steps: fit a choice model to historical transactions, then optimize prices and assortments as if the fitted model were the truth. Chen, Owen, Pixton and Simchi-Levi (Management Science, 2021; author manuscript SSRN 2579462) ask how much revenue this "estimate, then optimize" procedure loses, as a function of the amount and richness of the historical data. Their answer is a non-asymptotic, high-probability bound on the revenue gap for a feature-dependent multinomial logit model that covers personalized pricing and personalized assortment in one framework.
The estimation side builds on the econometrics of the conditional logit model (McFadden, 1974), whose classical theory is asymptotic. The finite-sample tools come from high-dimensional statistics: concentration of sample covariance matrices of sub-Gaussian vectors (Vershynin, 2012) and strong-convexity arguments for M-estimators.
There are products and a no-purchase option . A customer arrives with a feature vector , scaled so that . The seller offers an assortment and sets a price for each product, ; the price box is . For product the feature–price vector is .
The parameter is . The mean utility of product is . Under the multinomial logit (MNL) model the customer buys with probability
and buys nothing with probability . The expected revenue is .
The data are past transactions , where is the observed choice. The negative log-likelihood is . Given a radius with , the constrained MLE minimizes over .
Two assumptions govern the data. Assumption 1: the outcomes are conditionally independent given features and prices and follow the MNL model at the true parameter , and for each the vectors are independent across (not necessarily identically distributed) and sub-Gaussian with norm at most . Assumption 2: every product was offered in at least transactions, and the averaged second-moment matrix over the transactions offering has smallest eigenvalue at least .
Given a family of feasible assortments, maximizes over (the oracle decision) and maximizes .
For every there is , and for every a constant , such that whenever , with probability at least , for every feature vector ,
The constants are unspecified, as on the page; only their dependence is fixed.
The result. The theorem quantifies the value of historical data for personalized revenue management. The loss shrinks as and degrades with (products rarely offered in the past) and (features and prices that are nearly collinear in the data). This makes precise two practical warnings of the paper: price experimentation must not be correlated with customer features, and every product must have been explored. The bound is uniform over customers, so it is an out-of-sample guarantee. It specializes to customized pricing (Corollary 1) and to personalized assortment with fixed prices (Corollary 2), and the parameter rate of Theorem 1 matches the Cramér–Rao rate up to logarithmic factors.
Formalizing it. The paper's results are proved but none has been machine-checked. A formal development would produce a verified finite-sample theory of the constrained logit MLE: the softmax Hessian bound, strong convexity of the log-likelihood with high probability, the gradient concentration, and the transfer to revenue. Two printed statements need care, and the mission states the corrected forms: Lemma 2 needs an additional sample-size condition (see Formalization scope), and the printed (5) loses a factor relative to what Theorem 1 uses.
The deterministic parts (Lemma EC.1, the constant , the Lipschitz bound, the step (4)–(5)) are finite-dimensional calculus. The main obstacle is Lemma 2. Its proof needs the empirical second-moment matrices to be within of their expectations in operator norm, for independent but non-identically distributed sub-Gaussian vectors, with a sample size depending on only through a constant. The standard references state this for identically distributed vectors. Mathlib has no matrix concentration of this kind, and an -net argument with a Bernstein-type bound must be built. A second obstacle is the randomness of the decision itself: the optimal decisions are argmax selections, so the bad event is controlled through Theorem 1's event and not through measurability of the decision.
A first attempt often tries to bound the gap by the parameter error directly through the optimization problem. That fails: the argmax is not Lipschitz in . The paper's route compares revenues of fixed decisions, which needs the bound of Proposition 1 uniformly over all decisions.
The model is one definitions file in the namespace PersonalizedRM.RevenueGap. The parameter is EuclideanSpace ℝ (Fin J × Fin (d+1)), so ‖θ‖ is the Euclidean norm; is an explicit sum and is a bound on every fderiv partial derivative. Outcomes are Option (Fin J) (none is no purchase). Historical assortments are deterministic. The conventions committed to are:
Theorem 1, Proposition 1 and Theorem 2 are stated exactly as printed.
Constant order. The constants are quantified in the order , before , , , , and the data. A constant chosen after the data could be made large enough that the right-hand side exceeds the trivial bounds (revenue gap , parameter error ), and the statements would be empty.
Infrastructure. A complete development needs:
The concentration bound and the softmax Hessian bound are reusable beyond this mission. Contributions to any milestone are welcome, as are proofs of the generic lemmas as separate theorems.
Not formalized: Corollaries 1–2 (specializations of the goal), Proposition 2 (the mixing-data rate, stated only up to ), and the numerical study of §5.
Ride-hailing, car-sharing and bike-sharing platforms price trips whose execution moves the resource itself: a car that takes a passenger from the suburbs to the airport is no longer available in the suburbs. Each price therefore sets both the revenue of the current request and the future spatial distribution of the fleet. Choosing prices to maximise long-run revenue is a Markov decision problem whose state, the number of resources at each location, has a number of configurations exponential in the number of locations. Exact dynamic programming is impossible at the scale of a city.
Balseiro, Brown and Chen (SSRN 3313737, version of May 23, 2020; published in Management Science, doi:10.1287/mnsc.2020.3735) study hub-and-spoke networks and propose a Lagrangian policy. The capacity constraint coupling the locations is relaxed with a dual variable, the relaxation separates into one small problem per spoke, and the per-spoke solutions are implemented in the real system. Earlier work on this model (Waserhole and Jost, 2016; Banerjee, Freund and Lykouris, 2016) uses fluid relaxations that lead to static prices, depending on the origin and destination but not on the resource levels. These are within a factor of the fluid bound, hence asymptotically optimal when the number of resources grows faster than the number of locations . When and grow at the same rate, which is the regime of a large city with few vehicles per area, no static policy is asymptotically optimal (the paper's Example 5.1). The Lagrangian policy is a dynamic, state-dependent policy that is computable and asymptotically optimal in that regime.
A hub (location ) and spokes share resources. In each period one request arrives: it asks to relocate a resource from spoke to the hub, type , with probability , or from the hub to spoke , type , with probability ; these probabilities sum to one and are independent across periods. The provider picks a demand level , equivalently a price. The request is fulfilled with probability if its origin holds a resource and is lost otherwise; the expected revenue is . Assumption 2.1: each is strictly concave on , , , , and the maximiser is interior.
The state is the vector of spoke levels , the hub holding . The optimal average revenue (problem (1)) is the supremum, over non-anticipative feasible policies, of the long-run average expected revenue.
Penalising the spoke resources with a dual variable yields, for each spoke, the spoke problem (6): maximise over a distribution on and controls satisfying the birth–death balance equations . Its value is . The relaxation value is (4), the Lagrangian bound is (9), and the perturbed dual is (11), with optimal solution . The Lagrangian policy (Definition 3.1) applies the controls of optimal solutions of (6) at , spoke by spoke, and drops a hub request when the hub is empty. is its average revenue and the stationary probability that the hub is empty. In the relaxed system the hub may go negative; there the spokes are independent with laws .
Under Assumption 4.1 ( for every spoke, independent of ) and with , for ,
and with ,
The milestones follow the paper's proof. The spoke problem solves the spoke Bellman equation (Proposition 3.2), the relaxation's value is independent of the initial state, equals and bounds (Proposition 3.1), and the controls are monotone (Proposition 3.3). The relaxed and original chains have stationary laws and a unique (Corollaries B.10, B.11). The perturbation costs at most (Lemma 4.2), continuation-value differences are at most (Lemma A.10), and the relaxed–original gap is controlled by hub depletion (Lemma 4.3), giving Theorem 4.1,
Stochastic dominance between the two systems (Lemma 4.4) gives (Corollary 4.5). The spoke laws are log-concave (Proposition B.9), log-concave generating functions are dominated by geometric ones (Lemma A.14), a concentration bound for sums of log-concave variables follows (Lemma A.12), and the relaxed depletion probability is at most (Proposition 4.6).
The result. A policy computed from independent problems of size loses only per period against the optimal policy of a problem with exponentially many states. No static policy achieves a vanishing gap. Theorem 4.1 also yields a practical certificate: is a computable upper bound, and the gap is governed by one observable quantity, the hub-depletion probability. The same structure extends to several hubs (the paper's Theorem 6.1).
Formalizing it. The result is proved in the paper; nothing here is open, and no part of it has been machine-checked. A formal proof would check a chain that combines average-reward dynamic programming, convex duality and sensitivity analysis, a coupling argument between two Markov chains, and a concentration inequality for log-concave variables. Several of these steps are stated in the paper with brief or cited arguments (the Bellman equation of the spoke problem, the class structure of the chains, Keilson's factorial-moment inequality behind Lemma A.14).
The natural first idea is to use the Lagrangian policy at the optimal dual of (9). At the relaxation keeps zero resources in the hub in expectation, so the real hub is empty a constant fraction of the time and every hub request lost there costs a constant. The perturbation is what makes the argument work. The key step is then to compare the relaxed system, where spokes are independent and the hub may go negative, with the original system, where the hub constraint couples all spokes. This needs both a loss bound per depletion event (Lemma A.10, which rests on the monotonicity of Proposition 3.3) and a pathwise coupling (Lemma 4.4). A Chebyshev bound on the hub level gives only a polynomial rate. The exponential rate requires the log-concavity of every spoke law and a geometric domination of its generating function.
limsup of its time average. Stationary distributions are finite probability vectors, via the published definition MarkovChain.IsStationary. Sums of independent ℕ-valued variables are iterated convolutions.Fin n ⊕ Fin n, spoke levels Fin (m+1), the hub level is , and the original chain lives on .Retailers, online travel agencies and search engines display products in an ordered list or on a physical layout, and customers inspect only a prefix of it. Display optimization asks how to assign products to positions so as to maximize expected revenue when each customer considers only the products shown in the first positions, with random. Aouad and Segev (SSRN 2709652; Management Science 67(6), 2021) study this problem with vertically differentiated locations (every customer who sees position also sees positions ) and multinomial logit (MNL) choice within the consideration set. The model covers assortment planning over time and product framing on web pages, and it was calibrated on Expedia hotel-search data in the paper's case study.
The paper's headline claim (Theorem 1.1) is a polynomial-time approximation scheme, obtained by a dynamic program over approximate assortments followed by a rounding of its actions into an assignment. The rounding analysis, Section 5.2, contains a self-contained chain of combinatorial inequalities about the rounded assignment. That chain is the subject of this mission.
There are items. Item has a price and an MNL preference weight ; write and, for an assortment ,
the expected revenue of offering to an MNL customer with a no-purchase option of weight . An assignment is a bijection from positions to items; is the set of items in positions , , and with position weights the objective is
The algorithm fixes an accuracy and a guessed position . A sequence of dynamic-programming actions consists of events and pairs of item sets (a sub-assortment and a super-assortment), starting from , and ending at , . Consecutive actions must satisfy seven constraints, (8)–(14) of the paper: nestedness , the accuracy bounds and the same for , a cardinality constraint linking sets to events, and three growth conditions on the proxies
depending on the position of relative to . With the last index whose event is at most , the actions are rounded into blocks of new items (from before , from after), and the rounded assignment lists the blocks in order, each by non-increasing price. The block boundaries are , and are the position intervals between consecutive boundaries, split at .
For every , every feasible action sequence and every rounded assignment ,
with . This is inequality (15) of the paper combined with (16), in the proof of Lemma 5.4.
The goal is the step that converts the dynamic program's value into a revenue guarantee for an actual assignment: whatever action sequence the dynamic program returns, the assignment built from it earns at least times the interval-weighted minima of the program's proxies. Any repaired analysis of the scheme has to pass through a statement of this form, since the rounding of §4.4 is the only link between the program's actions and a display.
The remaining half of the paper's argument is not true as printed. Lemma 5.4, , and with it the approximation clause of Theorem 1.1, fail for the paper's own algorithm: with , , , and , no feasible action sequence can place item 2 first, and every rounded assignment earns at most against an optimum of . A formal proof of the true half isolates precisely where the published argument stops working. No part of this chain has a machine-checked proof.
The rounding discards items. Before , block keeps only the part of the sub-assortment that is new with respect to , so the prefix of can carry less -mass than . A loss bounded by the per-step accuracy would accumulate over up to steps; Lemma 5.2's constant is independent of , and holds only because the growth constraint forces to grow geometrically, which the obvious step-by-step bound does not use. The second obstacle is that the revenue between two block boundaries is not monotone; bounding it by the boundary values requires the unimodality of Claim 5.5, which depends on the price order inside each block and on the MNL convex-combination structure, not on the dynamic program.
Items are Fin n; positions and DP indices are 1-based natural numbers as on the page, and an assignment is an equivalence Fin n ≃ Fin n from the 0-based position to the item at position . A DP sequence stores events and set pairs as functions on ℕ, read through accessors implementing the root convention , and . Feasibility is exactly the boundary and root conditions plus (8)–(14), with (11) written without natural-number truncation and (14) in the lower-bound form printed on p. 19. The rounded assignment is a predicate: block contents fixed by , non-increasing prices within a block, ties in any order.
Conventions and additions relative to the page:
Feasibility and rounding are the page's constructions; neither predicate builds in Lemma 5.2, Lemma 5.3 or any revenue property, so the goal cannot be obtained by unfolding a hypothesis. A sorry-free sanity check exhibits an instance (, ) satisfying all hypotheses at once.
The development needs only finite sums over Finset, real arithmetic and induction over the block index. Contributions of all milestones are welcome; the identity and Claim 5.5 are reusable for any MNL ranking or display model.